Theorem mh 879

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 v c) ^ (b v d)) = (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))

Proof of Theorem mh

Step	Hyp	Ref	Expression
1		leao1 162	. . . . . 6 (a ^ b) =< (a v c)
2		leao2 163	. . . . . 6 (a ^ b) =< (b v d)
3	1, 2	ler2an 173	. . . . 5 (a ^ b) =< ((a v c) ^ (b v d))
4		leao1 162	. . . . . 6 (a ^ d) =< (a v c)
5		leao4 165	. . . . . 6 (a ^ d) =< (b v d)
6	4, 5	ler2an 173	. . . . 5 (a ^ d) =< ((a v c) ^ (b v d))
7	3, 6	lel2or 170	. . . 4 ((a ^ b) v (a ^ d)) =< ((a v c) ^ (b v d))
8		leao3 164	. . . . . 6 (c ^ b) =< (a v c)
9		leao2 163	. . . . . 6 (c ^ b) =< (b v d)
10	8, 9	ler2an 173	. . . . 5 (c ^ b) =< ((a v c) ^ (b v d))
11		leao3 164	. . . . . 6 (c ^ d) =< (a v c)
12		leao4 165	. . . . . 6 (c ^ d) =< (b v d)
13	11, 12	ler2an 173	. . . . 5 (c ^ d) =< ((a v c) ^ (b v d))
14	10, 13	lel2or 170	. . . 4 ((c ^ b) v (c ^ d)) =< ((a v c) ^ (b v d))
15	7, 14	lel2or 170	. . 3 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) =< ((a v c) ^ (b v d))
16		anass 76	. . . . . . 7 ((((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) ^ ((a ^ b) v (c ^ d))') = (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))'))
17	16	ax-r1 35	. . . . . 6 (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))')) = ((((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) ^ ((a ^ b) v (c ^ d))')
18		an4 86	. . . . . . . . 9 (((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) = (((a v c) ^ (c' v b')) ^ ((b v d) ^ (a' v 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 v c) ^ (c' v b')) ^ ((b v d) ^ (a' v d'))) = (((a ^ c') ^ (b ^ d')) v ((c ^ b') ^ (d ^ a')))
24	18, 23	ax-r2 36	. . . . . . . 8 (((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) = (((a ^ c') ^ (b ^ d')) v ((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) v (c ^ d))
29	27, 28	letr 137	. . . . . . . . 9 ((a ^ c') ^ (b ^ d')) =< ((a ^ b) v (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) v (c ^ d))
34	32, 33	letr 137	. . . . . . . . 9 ((c ^ b') ^ (d ^ a')) =< ((a ^ b) v (c ^ d))
35	29, 34	lel2or 170	. . . . . . . 8 (((a ^ c') ^ (b ^ d')) v ((c ^ b') ^ (d ^ a'))) =< ((a ^ b) v (c ^ d))
36	24, 35	bltr 138	. . . . . . 7 (((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) =< ((a ^ b) v (c ^ d))
37	36	leran 153	. . . . . 6 ((((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) ^ ((a ^ b) v (c ^ d))') =< (((a ^ b) v (c ^ d)) ^ ((a ^ b) v (c ^ d))')
38	17, 37	bltr 138	. . . . 5 (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))')) =< (((a ^ b) v (c ^ d)) ^ ((a ^ b) v (c ^ d))')
39		anor3 90	. . . . . . . 8 (((c ^ b) v (a ^ d))' ^ ((a ^ b) v (c ^ d))') = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))'
40	39	ax-r1 35	. . . . . . 7 (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))' = (((c ^ b) v (a ^ d))' ^ ((a ^ b) v (c ^ d))')
41		ax-a2 31	. . . . . . . . 9 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) = (((c ^ b) v (c ^ d)) v ((a ^ b) v (a ^ d)))
42		or12 80	. . . . . . . . . . . 12 ((c ^ d) v ((a ^ b) v (a ^ d))) = ((a ^ b) v ((c ^ d) v (a ^ d)))
43		ax-a3 32	. . . . . . . . . . . . 13 (((a ^ b) v (c ^ d)) v (a ^ d)) = ((a ^ b) v ((c ^ d) v (a ^ d)))
44	43	ax-r1 35	. . . . . . . . . . . 12 ((a ^ b) v ((c ^ d) v (a ^ d))) = (((a ^ b) v (c ^ d)) v (a ^ d))
45		ax-a2 31	. . . . . . . . . . . 12 (((a ^ b) v (c ^ d)) v (a ^ d)) = ((a ^ d) v ((a ^ b) v (c ^ d)))
46	42, 44, 45	3tr 65	. . . . . . . . . . 11 ((c ^ d) v ((a ^ b) v (a ^ d))) = ((a ^ d) v ((a ^ b) v (c ^ d)))
47	46	lor 70	. . . . . . . . . 10 ((c ^ b) v ((c ^ d) v ((a ^ b) v (a ^ d)))) = ((c ^ b) v ((a ^ d) v ((a ^ b) v (c ^ d))))
48		ax-a3 32	. . . . . . . . . 10 (((c ^ b) v (c ^ d)) v ((a ^ b) v (a ^ d))) = ((c ^ b) v ((c ^ d) v ((a ^ b) v (a ^ d))))
49		ax-a3 32	. . . . . . . . . 10 (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d))) = ((c ^ b) v ((a ^ d) v ((a ^ b) v (c ^ d))))
50	47, 48, 49	3tr1 63	. . . . . . . . 9 (((c ^ b) v (c ^ d)) v ((a ^ b) v (a ^ d))) = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))
51	41, 50	ax-r2 36	. . . . . . . 8 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))
52	51	ax-r4 37	. . . . . . 7 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))' = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))'
53		oran3 93	. . . . . . . . . 10 (c' v b') = (c ^ b)'
54		oran3 93	. . . . . . . . . 10 (a' v d') = (a ^ d)'
55	53, 54	2an 79	. . . . . . . . 9 ((c' v b') ^ (a' v d')) = ((c ^ b)' ^ (a ^ d)')
56		anor3 90	. . . . . . . . 9 ((c ^ b)' ^ (a ^ d)') = ((c ^ b) v (a ^ d))'
57	55, 56	ax-r2 36	. . . . . . . 8 ((c' v b') ^ (a' v d')) = ((c ^ b) v (a ^ d))'
58	57	ran 78	. . . . . . 7 (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))') = (((c ^ b) v (a ^ d))' ^ ((a ^ b