Theorem mh 861

Description: Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91.

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 154	. . . . . 6 (a ∩ b) ≤ (a ∪ c)
2		leao2 155	. . . . . 6 (a ∩ b) ≤ (b ∪ d)
3	1, 2	ler2an 165	. . . . 5 (a ∩ b) ≤ ((a ∪ c) ∩ (b ∪ d))
4		leao1 154	. . . . . 6 (a ∩ d) ≤ (a ∪ c)
5		leao4 157	. . . . . 6 (a ∩ d) ≤ (b ∪ d)
6	4, 5	ler2an 165	. . . . 5 (a ∩ d) ≤ ((a ∪ c) ∩ (b ∪ d))
7	3, 6	lel2or 162	. . . 4 ((a ∩ b) ∪ (a ∩ d)) ≤ ((a ∪ c) ∩ (b ∪ d))
8		leao3 156	. . . . . 6 (c ∩ b) ≤ (a ∪ c)
9		leao2 155	. . . . . 6 (c ∩ b) ≤ (b ∪ d)
10	8, 9	ler2an 165	. . . . 5 (c ∩ b) ≤ ((a ∪ c) ∩ (b ∪ d))
11		leao3 156	. . . . . 6 (c ∩ d) ≤ (a ∪ c)
12		leao4 157	. . . . . 6 (c ∩ d) ≤ (b ∪ d)
13	11, 12	ler2an 165	. . . . 5 (c ∩ d) ≤ ((a ∪ c) ∩ (b ∪ d))
14	10, 13	lel2or 162	. . . 4 ((c ∩ b) ∪ (c ∩ d)) ≤ ((a ∪ c) ∩ (b ∪ d))
15	7, 14	lel2or 162	. . 3 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) ≤ ((a ∪ c) ∩ (b ∪ d))
16		anass 69	. . . . . . 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 34	. . . . . 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 78	. . . . . . . . 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 860	. . . . . . . . 9 (((a ∪ c) ∩ (c⊥ ∪ b⊥ )) ∩ ((b ∪ d) ∩ (a⊥ ∪ d⊥ ))) = (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )))
24	18, 23	ax-r2 35	. . . . . . . 8 (((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) = (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )))
25		lea 152	. . . . . . . . . . 11 (a ∩ c⊥ ) ≤ a
26		lea 152	. . . . . . . . . . 11 (b ∩ d⊥ ) ≤ b
27	25, 26	le2an 161	. . . . . . . . . 10 ((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ≤ (a ∩ b)
28		leo 150	. . . . . . . . . 10 (a ∩ b) ≤ ((a ∩ b) ∪ (c ∩ d))
29	27, 28	letr 129	. . . . . . . . 9 ((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ≤ ((a ∩ b) ∪ (c ∩ d))
30		lea 152	. . . . . . . . . . 11 (c ∩ b⊥ ) ≤ c
31		lea 152	. . . . . . . . . . 11 (d ∩ a⊥ ) ≤ d
32	30, 31	le2an 161	. . . . . . . . . 10 ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )) ≤ (c ∩ d)
33		leor 151	. . . . . . . . . 10 (c ∩ d) ≤ ((a ∩ b) ∪ (c ∩ d))
34	32, 33	letr 129	. . . . . . . . 9 ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )) ≤ ((a ∩ b) ∪ (c ∩ d))
35	29, 34	lel2or 162	. . . . . . . 8 (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ ))) ≤ ((a ∩ b) ∪ (c ∩ d))
36	24, 35	bltr 130	. . . . . . 7 (((a ∪ c) ∩ (b ∪ d)) ∩ ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ ))) ≤ ((a ∩ b) ∪ (c ∩ d))
37	36	leran 145	. . . . . 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 130	. . . . 5 (((a ∪ c) ∩ (b ∪ d)) ∩ (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )) ≤ (((a ∩ b) ∪ (c ∩ d)) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
39		anor3 82	. . . . . . . 8 (((c ∩ b) ∪ (a ∩ d))⊥ ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ) = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))⊥
40	39	ax-r1 34	. . . . . . 7 (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))⊥ = (((c ∩ b) ∪ (a ∩ d))⊥ ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
41		ax-a2 30	. . . . . . . . 9 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) = (((c ∩ b) ∪ (c ∩ d)) ∪ ((a ∩ b) ∪ (a ∩ d)))
42		or12 73	. . . . . . . . . . . 12 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d))) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∩ d)))
43		ax-a3 31	. . . . . . . . . . . . 13 (((a ∩ b) ∪ (c ∩ d)) ∪ (a ∩ d)) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∩ d)))
44	43	ax-r1 34	. . . . . . . . . . . 12 ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∩ d))) = (((a ∩ b) ∪ (c ∩ d)) ∪ (a ∩ d))
45		ax-a2 30	. . . . . . . . . . . 12 (((a ∩ b) ∪ (c ∩ d)) ∪ (a ∩ d)) = ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d)))
46	42, 44, 45	3tr 62	. . . . . . . . . . 11 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d))) = ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d)))
47	46	lor 66	. . . . . . . . . 10 ((c ∩ b) ∪ ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d)))) = ((c ∩ b) ∪ ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d))))
48		ax-a3 31	. . . . . . . . . 10 (((c ∩ b) ∪ (c ∩ d)) ∪ ((a ∩ b) ∪ (a ∩ d))) = ((c ∩ b) ∪ ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∩ d))))
49		ax-a3 31	. . . . . . . . . 10 (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d))) = ((c ∩ b) ∪ ((a ∩ d) ∪ ((a ∩ b) ∪ (c ∩ d))))
50	47, 48, 49	3tr1 60	. . . . . . . . 9 (((c ∩ b) ∪ (c ∩ d)) ∪ ((a ∩ b) ∪ (a ∩ d))) = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))
51	41, 50	ax-r2 35	. . . . . . . 8 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))
52	51	ax-r4 36	. . . . . . 7 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ = (((c ∩ b) ∪ (a ∩ d)) ∪ ((a ∩ b) ∪ (c ∩ d)))⊥
53		oran3 85	. . . . . . . . . 10 (c⊥ ∪ b⊥ ) = (c ∩ b)⊥
54		oran3 85	. . . . . . . . . 10 (a⊥ ∪ d⊥ ) = (a ∩ d)⊥
55	53, 54	2an 72	. . . . . . . . 9 ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) = ((c ∩ b)⊥ ∩ (a ∩ d)⊥ )
56		anor3 82	. . . . . . . . 9 ((c ∩ b)⊥ ∩ (a ∩ d)⊥ ) = ((c ∩ b) ∪ (a ∩ d))⊥
57	55, 56	ax-r2 35	. . . . . . . 8 ((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) = ((c ∩ b) ∪ (a ∩ d))⊥
58	57	ran 71	. . . . . . 7 (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ ) = (((c ∩ b) ∪ (a ∩ d))⊥ ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
59	40, 52, 58	3tr1 60	. . . . . 6 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ = (((c⊥ ∪ b⊥ ) ∩ (a⊥ ∪ d⊥ )) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
60	59	lan 70	. . . . 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 93	. . . . 5 0 = (((a ∩ b) ∪ (c ∩ d)) ∩ ((a ∩ b) ∪ (c ∩ d))⊥ )
62	38, 60, 61	le3tr1 132	. . . 4 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ ) ≤ 0
63		le0 139	. . . 4 0 ≤ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ )
64	62, 63	lebi 137	. . 3 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))⊥ ) = 0
65	15, 64	oml3 434	. 2 (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d))) = ((a ∪ c) ∩ (b ∪ d))
66	65	ax-r1 34	1 ((a ∪ c) ∩ (b ∪ d)) = (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))

Syntax hints:   = wb 1   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 10

This theorem is referenced by:  mh2 866  mlaconjo 868

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org