Theorem mhlem 876

Description: Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)

Hypothesis

Ref	Expression
mhlem.1	(a ∪ b) ≤ (c ∪ d)⊥

Assertion

Ref	Expression
mhlem	((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))

Proof of Theorem mhlem

Step	Hyp	Ref	Expression
1		comor1 461	. . . . . . 7 (a ∪ b) C a
2		comor2 462	. . . . . . 7 (a ∪ b) C b
3	1, 2	com2an 484	. . . . . 6 (a ∪ b) C (a ∩ b)
4		mhlem.1	. . . . . . . 8 (a ∪ b) ≤ (c ∪ d)⊥
5	4	lecom 180	. . . . . . 7 (a ∪ b) C (c ∪ d)⊥
6	5	comcom7 460	. . . . . 6 (a ∪ b) C (c ∪ d)
7	3, 6	fh1r 473	. . . . 5 (((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) = (((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b)))
8		comor1 461	. . . . . . 7 (c ∪ d) C c
9		comor2 462	. . . . . . 7 (c ∪ d) C d
10	8, 9	com2an 484	. . . . . 6 (c ∪ d) C (c ∩ d)
11		leao1 162	. . . . . . . . . 10 (a ∩ b) ≤ (a ∪ b)
12	11, 4	letr 137	. . . . . . . . 9 (a ∩ b) ≤ (c ∪ d)⊥
13	12	lecom 180	. . . . . . . 8 (a ∩ b) C (c ∪ d)⊥
14	13	comcom7 460	. . . . . . 7 (a ∩ b) C (c ∪ d)
15	14	comcom 453	. . . . . 6 (c ∪ d) C (a ∩ b)
16	10, 15	fh2rc 480	. . . . 5 (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d)) = (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (c ∩ d)))
17	7, 16	2or 72	. . . 4 ((((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) ∪ (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d))) = ((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (c ∩ d))))
18	11	lerr 150	. . . . . . . 8 (a ∩ b) ≤ ((c ∩ d) ∪ (a ∪ b))
19	18	lecom 180	. . . . . . 7 (a ∩ b) C ((c ∩ d) ∪ (a ∪ b))
20	14, 19	fh3 471	. . . . . 6 ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b)))) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b))))
21		id 59	. . . . . . . 8 ((a ∪ c) ∩ (b ∪ d)) = ((a ∪ c) ∩ (b ∪ d))
22	4	mhlemlem1 874	. . . . . . . . 9 (((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) = (a ∪ c)
23	4	mhlemlem2 875	. . . . . . . . 9 (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d))) = (b ∪ d)
24	22, 23	2an 79	. . . . . . . 8 ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d)))) = ((a ∪ c) ∩ (b ∪ d))
25	21, 21, 24	3tr1 63	. . . . . . 7 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d))))
26		an4 86	. . . . . . . 8 ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d)))) = ((((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)) ∩ ((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))))
27		ancom 74	. . . . . . . 8 ((((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)) ∩ ((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d)))) = (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)))
28		ax-a2 31	. . . . . . . . . . 11 ((a ∪ b) ∪ (c ∩ d)) = ((c ∩ d) ∪ (a ∪ b))
29	11	df-le2 131	. . . . . . . . . . . . 13 ((a ∩ b) ∪ (a ∪ b)) = (a ∪ b)
30	29	lor 70	. . . . . . . . . . . 12 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∪ b))) = ((c ∩ d) ∪ (a ∪ b))
31	30	ax-r1 35	. . . . . . . . . . 11 ((c ∩ d) ∪ (a ∪ b)) = ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∪ b)))
32		or12 80	. . . . . . . . . . 11 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∪ b))) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b)))
33	28, 31, 32	3tr 65	. . . . . . . . . 10 ((a ∪ b) ∪ (c ∩ d)) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b)))
34	33	lan 77	. . . . . . . . 9 (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d))) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b))))
35		leo 158	. . . . . . . . . . . . . . . 16 a ≤ (a ∪ b)
36	35, 4	letr 137	. . . . . . . . . . . . . . 15 a ≤ (c ∪ d)⊥
37	36	lecom 180	. . . . . . . . . . . . . 14 a C (c ∪ d)⊥
38	37	comcom7 460	. . . . . . . . . . . . 13 a C (c ∪ d)
39	38	comcom 453	. . . . . . . . . . . 12 (c ∪ d) C a
40		leor 159	. . . . . . . . . . . . . . . 16 b ≤ (a ∪ b)
41	40, 4	letr 137	. . . . . . . . . . . . . . 15 b ≤ (c ∪ d)⊥
42	41	lecom 180	. . . . . . . . . . . . . 14 b C (c ∪ d)⊥
43	42	comcom7 460	. . . . . . . . . . . . 13 b C (c ∪ d)
44	43	comcom 453	. . . . . . . . . . . 12 (c ∪ d) C b
45	39, 44	fh3r 475	. . . . . . . . . . 11 ((a ∩ b) ∪ (c ∪ d)) = ((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d)))
46		leo 158	. . . . . . . . . . . . . . . 16 c ≤ (c ∪ d)
47	4	lecon3 157	. . . . . . . . . . . . . . . 16 (c ∪ d) ≤ (a ∪ b)⊥
48	46, 47	letr 137	. . . . . . . . . . . . . . 15 c ≤ (a ∪ b)⊥
49	48	lecom 180	. . . . . . . . . . . . . 14 c C (a ∪ b)⊥
50	49	comcom7 460	. . . . . . . . . . . . 13 c C (a ∪ b)
51	50	comcom 453	. . . . . . . . . . . 12 (a ∪ b) C c
52		leor 159	. . . . . . . . . . . . . . . 16 d ≤ (c ∪ d)
53	52, 47	letr 137	. . . . . . . . . . . . . . 15 d ≤ (a ∪ b)⊥
54	53	lecom 180	. . . . . . . . . . . . . 14 d C (a ∪ b)⊥
55	54	comcom7 460	. . . . . . . . . . . . 13 d C (a ∪ b)
56	55	comcom 453	. . . . . . . . . . . 12 (a ∪ b) C d
57	51, 56	fh3 471	. . . . . . . . . . 11 ((a ∪ b) ∪ (c ∩ d)) = (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))
58	45, 57	2an 79	. . . . . . . . . 10 (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d))) = (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)))
59	58	ax-r1 35	. . . . . . . . 9 (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d)))
60	34, 59, 20	3tr1 63	. . . . . . . 8 (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))) = ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b))))
61	26, 27, 60	3tr 65	. . . . . . 7 ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d)))) = ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b))))
62	25, 61	ax-r2 36	. . . . . 6 ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b))))
63	20, 62, 34	3tr1 63	. . . . 5 ((a ∪ c) ∩ (b ∪ d)) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d)))
64	3, 6	com2or 483	. . . . . 6 (a ∪ b) C ((a ∩ b) ∪ (c ∪ d))
65		leao1 162	. . . . . . . . . 10 (c ∩ d) ≤ (c ∪ d)
66	65, 47	letr 137	. . . . . . . . 9 (c ∩ d) ≤ (a ∪ b)⊥
67	66	lecom 180	. . . . . . . 8 (c ∩ d) C (a ∪ b)⊥
68	67	comcom7 460	. . . . . . 7 (c ∩ d) C (a ∪ b)
69	68	comcom 453	. . . . . 6 (a ∪ b) C (c ∩ d)
70	64, 69	fh2 470	. . . . 5 (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d))) = ((((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) ∪ (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d)))
71	63, 70	ax-r2 36	. . . 4 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) ∪ (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d)))
72		ax-a3 32	. . . 4 (((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) ∪ ((c ∪ d) ∩ (c ∩ d))) = ((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (c ∩ d))))
73	17, 71, 72	3tr1 63	. . 3 ((a ∪ c) ∩ (b ∪ d)) = (((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) ∪ ((c ∪ d) ∩ (c ∩ d)))
74		ax-a3 32	. . . 4 ((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) = (((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))))
75	74	ax-r5 38	. . 3 (((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) ∪ ((c ∪ d) ∩ (c ∩ d))) = ((((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) ∪ ((c ∪ d) ∩ (c ∩ d)))
76	73, 75	ax-r2 36	. 2 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) ∪ ((c ∪ d) ∩ (c ∩ d)))
77	11, 65	le2an 169	. . . . . . . . 9 ((a ∩ b) ∩ (c ∩ d)) ≤ ((a ∪ b) ∩ (c ∪ d))
78		ancom 74	. . . . . . . . 9 ((a ∪ b) ∩ (c ∪ d)) = ((c ∪ d) ∩ (a ∪ b))
79	77, 78	lbtr 139	. . . . . . . 8 ((a ∩ b) ∩ (c ∩ d)) ≤ ((c ∪ d) ∩ (a ∪ b))
80	79	df-le2 131	. . . . . . 7 (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (a ∪ b))) = ((c ∪ d) ∩ (a ∪ b))
81		ax-a2 31	. . . . . . 7 (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))) = (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (a ∪ b)))
82	80, 81, 78	3tr1 63	. . . . . 6 (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))) = ((a ∪ b) ∩ (c ∪ d))
83	4	ortha 438	. . . . . 6 ((a ∪ b) ∩ (c ∪ d)) = 0
84	82, 83	ax-r2 36	. . . . 5 (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))) = 0
85	84	lor 70	. . . 4 (((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) = (((a ∩ b) ∩ (a ∪ b)) ∪ 0)
86		or0 102	. . . 4 (((a ∩ b) ∩ (a ∪ b)) ∪ 0) = ((a ∩ b) ∩ (a ∪ b))
87	11	df2le2 136	. . . 4 ((a ∩ b) ∩ (a ∪ b)) = (a ∩ b)
88	85, 86, 87	3tr 65	. . 3 (((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) = (a ∩ b)
89		lear 161	. . . 4 ((c ∪ d) ∩ (c ∩ d)) ≤ (c ∩ d)
90		leid 148	. . . . 5 (c ∩ d) ≤ (c ∩ d)
91	65, 90	ler2an 173	. . . 4 (c ∩ d) ≤ ((c ∪ d) ∩ (c ∩ d))
92	89, 91	lebi 145	. . 3 ((c ∪ d) ∩ (c ∩ d)) = (c ∩ d)
93	88, 92	2or 72	. 2 ((((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) ∪ ((c ∪ d) ∩ (c ∩ d))) = ((a ∩ b) ∪ (c ∩ d))
94	76, 93	ax-r2 36	1 ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  mhlem2  878