Theorem mhlem 858

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 443	. . . . . . 7 (a v b) C a
2		comor2 444	. . . . . . 7 (a v b) C b
3	1, 2	com2an 466	. . . . . 6 (a v b) C (a ^ b)
4		mhlem.1	. . . . . . . 8 (a v b) =< (c v d)_|_
5	4	lecom 172	. . . . . . 7 (a v b) C (c v d)_|_
6	5	comcom7 442	. . . . . 6 (a v b) C (c v d)
7	3, 6	fh1r 455	. . . . 5 (((a ^ b) v (c v d)) ^ (a v b)) = (((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b)))
8		comor1 443	. . . . . . 7 (c v d) C c
9		comor2 444	. . . . . . 7 (c v d) C d
10	8, 9	com2an 466	. . . . . 6 (c v d) C (c ^ d)
11		leao1 154	. . . . . . . . . 10 (a ^ b) =< (a v b)
12	11, 4	letr 129	. . . . . . . . 9 (a ^ b) =< (c v d)_|_
13	12	lecom 172	. . . . . . . 8 (a ^ b) C (c v d)_|_
14	13	comcom7 442	. . . . . . 7 (a ^ b) C (c v d)
15	14	comcom 435	. . . . . 6 (c v d) C (a ^ b)
16	10, 15	fh2rc 462	. . . . 5 (((a ^ b) v (c v d)) ^ (c ^ d)) = (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (c ^ d)))
17	7, 16	2or 67	. . . 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 142	. . . . . . . 8 (a ^ b) =< ((c ^ d) v (a v b))
19	18	lecom 172	. . . . . . 7 (a ^ b) C ((c ^ d) v (a v b))
20	14, 19	fh3 453	. . . . . 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 58	. . . . . . . 8 ((a v c) ^ (b v d)) = ((a v c) ^ (b v d))
22	4	mhlemlem1 856	. . . . . . . . 9 (((a v b) v c) ^ (a v (c v d))) = (a v c)
23	4	mhlemlem2 857	. . . . . . . . 9 (((a v b) v d) ^ (b v (c v d))) = (b v d)
24	22, 23	2an 72	. . . . . . . 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 60	. . . . . . 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 78	. . . . . . . 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 68	. . . . . . . 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 30	. . . . . . . . . . 11 ((a v b) v (c ^ d)) = ((c ^ d) v (a v b))
29	11	df-le2 123	. . . . . . . . . . . . 13 ((a ^ b) v (a v b)) = (a v b)
30	29	lor 66	. . . . . . . . . . . 12 ((c ^ d) v ((a ^ b) v (a v b))) = ((c ^ d) v (a v b))
31	30	ax-r1 34	. . . . . . . . . . 11 ((c ^ d) v (a v b)) = ((c ^ d) v ((a ^ b) v (a v b)))
32		or12 73	. . . . . . . . . . 11 ((c ^ d) v ((a ^ b) v (a v b))) = ((a ^ b) v ((c ^ d) v (a v b)))
33	28, 31, 32	3tr 62	. . . . . . . . . 10 ((a v b) v (c ^ d)) = ((a ^ b) v ((c ^ d) v (a v b)))
34	33	lan 70	. . . . . . . . 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 150	. . . . . . . . . . . . . . . 16 a =< (a v b)
36	35, 4	letr 129	. . . . . . . . . . . . . . 15 a =< (c v d)_|_
37	36	lecom 172	. . . . . . . . . . . . . 14 a C (c v d)_|_
38	37	comcom7 442	. . . . . . . . . . . . 13 a C (c v d)
39	38	comcom 435	. . . . . . . . . . . 12 (c v d) C a
40		leor 151	. . . . . . . . . . . . . . . 16 b =< (a v b)
41	40, 4	letr 129	. . . . . . . . . . . . . . 15 b =< (c v d)_|_
42	41	lecom 172	. . . . . . . . . . . . . 14 b C (c v d)_|_
43	42	comcom7 442	. . . . . . . . . . . . 13 b C (c v d)
44	43	comcom 435	. . . . . . . . . . . 12 (c v d) C b
45	39, 44	fh3r 457	. . . . . . . . . . 11 ((a ^ b) v (c v d)) = ((a v (c v d)) ^ (b v (c v d)))
46		leo 150	. . . . . . . . . . . . . . . 16 c =< (c v d)
47	4	lecon3 149	. . . . . . . . . . . . . . . 16 (c v d) =< (a v b)_|_
48	46, 47	letr 129	. . . . . . . . . . . . . . 15 c =< (a v b)_|_
49	48	lecom 172	. . . . . . . . . . . . . 14 c C (a v b)_|_
50	49	comcom7 442	. . . . . . . . . . . . 13 c C (a v b)
51	50	comcom 435	. . . . . . . . . . . 12 (a v b) C c
52		leor 151	. . . . . . . . . . . . . . . 16 d =< (c v d)
53	52, 47	letr 129	. . . . . . . . . . . . . . 15 d =< (a v b)_|_
54	53	lecom 172	. . . . . . . . . . . . . 14 d C (a v b)_|_
55	54	comcom7 442	. . . . . . . . . . . . 13 d C (a v b)
56	55	comcom 435	. . . . . . . . . . . 12 (a v b) C d
57	51, 56	fh3 453	. . . . . . . . . . 11 ((a v b) v (c ^ d)) = (((a v b) v c) ^ ((a v b) v d))
58	45, 57	2an 72	. . . . . . . . . 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 34	. . . . . . . . 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 60	. . . . . . . 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 62	. . . . . . 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 35	. . . . . 6 ((a v c) ^ (b v d)) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
63	20, 62, 34	3tr1 60	. . . . 5 ((a v c) ^ (b v d)) = (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d)))
64	3, 6	com2or 465	. . . . . 6 (a v b) C ((a ^ b) v (c v d))
65		leao1 154	. . . . . . . . . 10 (c ^ d) =< (c v d)
66	65, 47	letr 129	. . . . . . . . 9 (c ^ d) =< (a v b)_|_
67	66	lecom 172	. . . . . . . 8 (c ^ d) C (a v b)_|_
68	67	comcom7 442	. . . . . . 7 (c ^ d) C (a v b)
69	68	comcom 435	. . . . . 6 (a v b) C (c ^ d)
70	64, 69	fh2 452	. . . . 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 35	. . . 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 31	. . . 4 (((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v ((a ^ b) ^ (c ^ d))) 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