Theorem mhlem 876

Description: Lemma 7.1 of Kalmbach, p. 91.

Hypothesis

Ref	Expression
mhlem.1	(a v b) =< (c v d)'

Assertion

Ref	Expression
mhlem	((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))

Proof of Theorem mhlem

Step	Hyp	Ref	Expression
1		comor1 461	. . . . . . 7 (a v b) C a
2		comor2 462	. . . . . . 7 (a v b) C b
3	1, 2	com2an 484	. . . . . 6 (a v b) C (a ^ b)
4		mhlem.1	. . . . . . . 8 (a v b) =< (c v d)'
5	4	lecom 180	. . . . . . 7 (a v b) C (c v d)'
6	5	comcom7 460	. . . . . 6 (a v b) C (c v d)
7	3, 6	fh1r 473	. . . . 5 (((a ^ b) v (c v d)) ^ (a v b)) = (((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b)))
8		comor1 461	. . . . . . 7 (c v d) C c
9		comor2 462	. . . . . . 7 (c v d) C d
10	8, 9	com2an 484	. . . . . 6 (c v d) C (c ^ d)
11		leao1 162	. . . . . . . . . 10 (a ^ b) =< (a v b)
12	11, 4	letr 137	. . . . . . . . 9 (a ^ b) =< (c v d)'
13	12	lecom 180	. . . . . . . 8 (a ^ b) C (c v d)'
14	13	comcom7 460	. . . . . . 7 (a ^ b) C (c v d)
15	14	comcom 453	. . . . . 6 (c v d) C (a ^ b)
16	10, 15	fh2rc 480	. . . . 5 (((a ^ b) v (c v d)) ^ (c ^ d)) = (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (c ^ d)))
17	7, 16	2or 72	. . . 4 ((((a ^ b) v (c v d)) ^ (a v b)) v (((a ^ b) v (c v d)) ^ (c ^ d))) = ((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (c ^ d))))
18	11	lerr 150	. . . . . . . 8 (a ^ b) =< ((c ^ d) v (a v b))
19	18	lecom 180	. . . . . . 7 (a ^ b) C ((c ^ d) v (a v b))
20	14, 19	fh3 471	. . . . . 6 ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b)))) = (((a ^ b) v (c v d)) ^ ((a ^ b) v ((c ^ d) v (a v b))))
21		id 59	. . . . . . . 8 ((a v c) ^ (b v d)) = ((a v c) ^ (b v d))
22	4	mhlemlem1 874	. . . . . . . . 9 (((a v b) v c) ^ (a v (c v d))) = (a v c)
23	4	mhlemlem2 875	. . . . . . . . 9 (((a v b) v d) ^ (b v (c v d))) = (b v d)
24	22, 23	2an 79	. . . . . . . 8 ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d)))) = ((a v c) ^ (b v d))
25	21, 21, 24	3tr1 63	. . . . . . 7 ((a v c) ^ (b v d)) = ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d))))
26		an4 86	. . . . . . . 8 ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d)))) = ((((a v b) v c) ^ ((a v b) v d)) ^ ((a v (c v d)) ^ (b v (c v d))))
27		ancom 74	. . . . . . . 8 ((((a v b) v c) ^ ((a v b) v d)) ^ ((a v (c v d)) ^ (b v (c v d)))) = (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d)))
28		ax-a2 31	. . . . . . . . . . 11 ((a v b) v (c ^ d)) = ((c ^ d) v (a v b))
29	11	df-le2 131	. . . . . . . . . . . . 13 ((a ^ b) v (a v b)) = (a v b)
30	29	lor 70	. . . . . . . . . . . 12 ((c ^ d) v ((a ^ b) v (a v b))) = ((c ^ d) v (a v b))
31	30	ax-r1 35	. . . . . . . . . . 11 ((c ^ d) v (a v b)) = ((c ^ d) v ((a ^ b) v (a v b)))
32		or12 80	. . . . . . . . . . 11 ((c ^ d) v ((a ^ b) v (a v b))) = ((a ^ b) v ((c ^ d) v (a v b)))
33	28, 31, 32	3tr 65	. . . . . . . . . 10 ((a v b) v (c ^ d)) = ((a ^ b) v ((c ^ d) v (a v b)))
34	33	lan 77	. . . . . . . . 9 (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d))) = (((a ^ b) v (c v d)) ^ ((a ^ b) v ((c ^ d) v (a v b))))
35		leo 158	. . . . . . . . . . . . . . . 16 a =< (a v b)
36	35, 4	letr 137	. . . . . . . . . . . . . . 15 a =< (c v d)'
37	36	lecom 180	. . . . . . . . . . . . . 14 a C (c v d)'
38	37	comcom7 460	. . . . . . . . . . . . 13 a C (c v d)
39	38	comcom 453	. . . . . . . . . . . 12 (c v d) C a
40		leor 159	. . . . . . . . . . . . . . . 16 b =< (a v b)
41	40, 4	letr 137	. . . . . . . . . . . . . . 15 b =< (c v d)'
42	41	lecom 180	. . . . . . . . . . . . . 14 b C (c v d)'
43	42	comcom7 460	. . . . . . . . . . . . 13 b C (c v d)
44	43	comcom 453	. . . . . . . . . . . 12 (c v d) C b
45	39, 44	fh3r 475	. . . . . . . . . . 11 ((a ^ b) v (c v d)) = ((a v (c v d)) ^ (b v (c v d)))
46		leo 158	. . . . . . . . . . . . . . . 16 c =< (c v d)
47	4	lecon3 157	. . . . . . . . . . . . . . . 16 (c v d) =< (a v b)'
48	46, 47	letr 137	. . . . . . . . . . . . . . 15 c =< (a v b)'
49	48	lecom 180	. . . . . . . . . . . . . 14 c C (a v b)'
50	49	comcom7 460	. . . . . . . . . . . . 13 c C (a v b)
51	50	comcom 453	. . . . . . . . . . . 12 (a v b) C c
52		leor 159	. . . . . . . . . . . . . . . 16 d =< (c v d)
53	52, 47	letr 137	. . . . . . . . . . . . . . 15 d =< (a v b)'
54	53	lecom 180	. . . . . . . . . . . . . 14 d C (a v b)'
55	54	comcom7 460	. . . . . . . . . . . . 13 d C (a v b)
56	55	comcom 453	. . . . . . . . . . . 12 (a v b) C d
57	51, 56	fh3 471	. . . . . . . . . . 11 ((a v b) v (c ^ d)) = (((a v b) v c) ^ ((a v b) v d))
58	45, 57	2an 79	. . . . . . . . . 10 (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d))) = (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d)))
59	58	ax-r1 35	. . . . . . . . 9 (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d))) = (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d)))
60	34, 59, 20	3tr1 63	. . . . . . . 8 (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d))) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
61	26, 27, 60	3tr 65	. . . . . . 7 ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d)))) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
62	25, 61	ax-r2 36	. . . . . 6 ((a v c) ^ (b v d)) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
63	20, 62, 34	3tr1 63	. . . . 5 ((a v c) ^ (b v d)) = (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d)))
64	3, 6	com2or 483	. . . . . 6 (a v b) C ((a ^ b) v (c v d))
65		leao1 162	. . . . . . . . . 10 (c ^ d) =< (c v d)
66	65, 47	letr 137	. . . . . . . . 9 (c ^ d) =< (a v b)'
67	66	lecom 180	. . . . . . . 8 (c ^ d) C (a v b)'
68	67	comcom7 460	. . . . . . 7 (c ^ d) C (a v b)
69	68	comcom 453	. . . . . 6 (a v b) C (c ^ d)
70	64, 69	fh2 470	. . . . 5 (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d))) = ((((a ^ b) v (c v d)) ^ (a v b)) v (((a ^ b) v (c v d)) ^ (c ^ d)))
71	63, 70	ax-r2 36	. . . 4 ((a v c) ^ (b v d)) = ((((a ^ b) v (c v d)) ^ (a v b)) v (((a ^ b) v (c v d)) ^ (c ^ d)))
72		ax-a3 32	. . . 4 (((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v ((a ^ b) ^ (c ^ d))) v ((c v d) ^ (c ^ d))) = (