Theorem mh 879

Description: Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)

Hypotheses

Ref	Expression
mh.1	a C c
mh.2	a C d
mh.3	b C c
mh.4	b C d

Assertion

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

Proof of Theorem mh

Step	Hyp	Ref	Expression
1		leao1 162	. . . . . 6 (a ∩ b) ≤ (a ∪ c)
2		leao2 163	. . . . . 6 (a ∩ b) ≤ (b ∪ d)
3	1, 2	ler2an 173	. . . . 5 (a ∩ b) ≤ ((a ∪ c) ∩ (b ∪ d))
4		leao1 162	. . . . . 6 (a ∩ d) ≤ (a ∪ c)
5		leao4 165	. . . . . 6 (a ∩ d) ≤ (b ∪ d)
6	4, 5	ler2an 173	. . . . 5 (a ∩ d) ≤ ((a ∪ c) ∩ (b ∪ d))
7	3, 6	lel2or 170	. . . 4 ((a ∩ b) ∪ (a ∩ d)) ≤ ((a ∪ c) ∩ (b ∪ d))
8		leao3 164	. . . . . 6 (c ∩ b) ≤ (a ∪ c)
9		leao2 163	. . . . . 6 (c ∩ b) ≤ (b ∪ d)
10	8, 9	ler2an 173	. . . . 5 (c ∩ b) ≤ ((a ∪ c) ∩ (b ∪ d))
11		leao3 164	. . . . . 6 (c ∩ d) ≤ (a ∪ c)
12		leao4 165	. . . . . 6 (c ∩ d) ≤ (b ∪ d)
13	11, 12	ler2an 173	. . . . 5 (c ∩ d) ≤ ((a ∪ c) ∩ (b ∪ d))
14	10, 13	lel2or 170	. . . 4 ((c ∩ b) ∪ (c ∩ d)) ≤ ((a ∪ c) ∩ (b ∪ d))
15	7, 14	lel2or 170	. . 3 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) ≤ ((a ∪ c) ∩ (b ∪ d))
16		anass 76	. . . . . . 7 ((((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ) = (((a ∪ c) ∩ (b ∪ d)) ∩ (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ))
17	16	ax-r1 35	. . . . . 6 (((a ∪ c) ∩ (b ∪ d)) ∩ (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )) = ((((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
18		an4 86	. . . . . . . . 9 (((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) = (((a ∪ c) ∩ (c⊥ ∪ b⊥ )) ∩ ((b ∪ d) ∩ (a⊥ ∪ d⊥ )))
19		mh.1	. . . . . . . . . 10 a C c
20		mh.2	. . . . . . . . . 10 a C d
21		mh.3	. . . . . . . . . 10 b C c
22		mh.4	. . . . . . . . . 10 b C d
23	19, 20, 21, 22	mhlem2 878	. . . . . . . . 9 (((a ∪ c) ∩ (c⊥ ∪ b⊥ )) ∩ ((b ∪ d) ∩ (a⊥ ∪ d⊥ ))) = (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )))
24	18, 23	ax-r2 36	. . . . . . . 8 (((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) = (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )))
25		lea 160	. . . . . . . . . . 11 (a ∩ c⊥ ) ≤ a
26		lea 160	. . . . . . . . . . 11 (b ∩ d⊥ ) ≤ b
27	25, 26	le2an 169	. . . . . . . . . 10 ((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ≤ (a ∩ b)
28		leo 158	. . . . . . . . . 10 (a ∩ b) ≤ ((a ∩ b) ∪ (c ∩ d))
29	27, 28	letr 137	. . . . . . . . 9 ((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ≤ ((a ∩ b) ∪ (c ∩ d))
30		lea 160	. . . . . . . . . . 11 (c ∩ b⊥ ) ≤ c
31		lea 160	. . . . . . . . . . 11 (d ∩ a⊥ ) ≤ d
32	30, 31	le2an 169	. . . . . . . . . 10 ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )) ≤ (c ∩ d)
33		leor 159	. . . . . . . . . 10 (c ∩ d) ≤ ((a ∩ b) ∪ (c ∩ d))
34	32, 33	letr 137	. . . . . . . . 9 ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )) ≤ ((a ∩ b) ∪ (c ∩ d))
35	29, 34	lel2or 170	. . . . . . . 8 (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ ))) ≤ ((a ∩ b) ∪ (c ∩ d))
36	24, 35	bltr 138	. . . . . . 7 (((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) ≤ ((a ∩ b) ∪ (c ∩ d))
37	36	leran 153	. . . . . 6 ((((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ) ≤ (((a ∩ b) ∪ (c ∩ d)) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
38	17, 37	bltr 138	. . . . 5 (((a ∪ c) ∩ (b ∪ d)) ∩ (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )) ≤ (((a ∩ b) ∪ (c ∩ d)) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
39		anor3 90	. . . . . . . 8 (((c ∩ b) ∪ (a ∩ d))⊥ ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ) = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))⊥
40	39	ax-r1 35	. . . . . . 7 (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))⊥ = (((c ∩ b) ∪ (a ∩ d))⊥ ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
41		ax-a2 31	. . . . . . . . 9 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) = (((c ∩ b) ∪ (c ∩ d)) ∪ ((a ∩ b) ∪ (a ∩ d)))
42		or12 80	. . . . . . . . . . . 12 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d))) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∩ d)))
43		ax-a3 32	. . . . . . . . . . . . 13 (((a ∩ b) ∪ (c ∩ d)) ∪ (a ∩ d)) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∩ d)))
44	43	ax-r1 35	. . . . . . . . . . . 12 ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∩ d))) = (((a ∩ b) ∪ (c ∩ d)) ∪ (a ∩ d))
45		ax-a2 31	. . . . . . . . . . . 12 (((a ∩ b) ∪ (c ∩ d)) ∪ (a ∩ d)) = ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d)))
46	42, 44, 45	3tr 65	. . . . . . . . . . 11 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d))) = ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d)))
47	46	lor 70	. . . . . . . . . 10 ((c ∩ b) ∪ ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d)))) = ((c ∩ b) ∪ ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d))))
48		ax-a3 32	. . . . . . . . . 10 (((c ∩ b) ∪ (c ∩ d)) ∪ ((a ∩ b) ∪ (a ∩ d))) = ((c ∩ b) ∪ ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d))))
49		ax-a3 32	. . . . . . . . . 10 (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d))) = ((c ∩ b) ∪ ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d))))
50	47, 48, 49	3tr1 63	. . . . . . . . 9 (((c ∩ b) ∪ (c ∩ d)) ∪ ((a ∩ b) ∪ (a ∩ d))) = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))
51	41, 50	ax-r2 36	. . . . . . . 8 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))
52	51	ax-r4 37	. . . . . . 7 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))⊥
53		oran3 93	. . . . . . . . . 10 (c⊥ ∪ b⊥ ) = (c ∩ b)⊥
54		oran3 93	. . . . . . . . . 10 (a⊥ ∪ d⊥ ) = (a ∩ d)⊥
55	53, 54	2an 79	. . . . . . . . 9 ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) = ((c ∩ b)⊥ ∩ (a ∩ d)⊥ )
56		anor3 90	. . . . . . . . 9 ((c ∩ b)⊥ ∩ (a ∩ d)⊥ ) = ((c ∩ b) ∪ (a ∩ d))⊥
57	55, 56	ax-r2 36	. . . . . . . 8 ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) = ((c ∩ b) ∪ (a ∩ d))⊥
58	57	ran 78	. . . . . . 7 (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ) = (((c ∩ b) ∪ (a ∩ d))⊥ ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
59	40, 52, 58	3tr1 63	. . . . . 6 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ = (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
60	59	lan 77	. . . . 5 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ ) = (((a ∪ c) ∩ (b ∪ d)) ∩ (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ))
61		dff 101	. . . . 5 0 = (((a ∩ b) ∪ (c ∩ d)) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
62	38, 60, 61	le3tr1 140	. . . 4 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ ) ≤ 0
63		le0 147	. . . 4 0 ≤ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ )
64	62, 63	lebi 145	. . 3 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ ) = 0
65	15, 64	oml3 452	. 2 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) = ((a ∪ c) ∩ (b ∪ d))
66	65	ax-r1 35	1 ((a ∪ c) ∩ (b ∪ d)) = (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))

This proof depends on syntax axioms:   = wb 1   C wc 3  ^⊥ 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:  mh2  884  mlaconjo  886