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 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 154	. . . . . 6 (a ^ b) =< (a v c)
2		leao2 155	. . . . . 6 (a ^ b) =< (b v d)
3	1, 2	ler2an 165	. . . . 5 (a ^ b) =< ((a v c) ^ (b v d))
4		leao1 154	. . . . . 6 (a ^ d) =< (a v c)
5		leao4 157	. . . . . 6 (a ^ d) =< (b v d)
6	4, 5	ler2an 165	. . . . 5 (a ^ d) =< ((a v c) ^ (b v d))
7	3, 6	lel2or 162	. . . 4 ((a ^ b) v (a ^ d)) =< ((a v c) ^ (b v d))
8		leao3 156	. . . . . 6 (c ^ b) =< (a v c)
9		leao2 155	. . . . . 6 (c ^ b) =< (b v d)
10	8, 9	ler2an 165	. . . . 5 (c ^ b) =< ((a v c) ^ (b v d))
11		leao3 156	. . . . . 6 (c ^ d) =< (a v c)
12		leao4 157	. . . . . 6 (c ^ d) =< (b v d)
13	11, 12	ler2an 165	. . . . 5 (c ^ d) =< ((a v c) ^ (b v d))
14	10, 13	lel2or 162	. . . 4 ((c ^ b) v (c ^ d)) =< ((a v c) ^ (b v d))
15	7, 14	lel2or 162	. . 3 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) =< ((a v c) ^ (b v d))
16		anass 69	. . . . . . 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 34	. . . . . 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 78	. . . . . . . . 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 860	. . . . . . . . 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 35	. . . . . . . 8 (((a v c) ^ (b v d)) ^ ((c_|_ v b_|_) ^ (a_|_ v d_|_))) = (((a ^ c_|_) ^ (b ^ d_|_)) v ((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) v (c ^ d))
29	27, 28	letr 129	. . . . . . . . 9 ((a ^ c_|_) ^ (b ^ d_|_)) =< ((a ^ b) v (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) v (c ^ d))
34	32, 33	letr 129	. . . . . . . . 9 ((c ^ b_|_) ^ (d ^ a_|_)) =< ((a ^ b) v (c ^ d))
35	29, 34	lel2or 162	. . . . . . . 8 (((a ^ c_|_) ^ (b ^ d_|_)) v ((c ^ b_|_) ^ (d ^ a_|_))) =< ((a ^ b) v (c ^ d))
36	24, 35	bltr 130	. . . . . . 7 (((a v c) ^ (b v d)) ^ ((c_|_ v b_|_) ^ (a_|_ v d_|_))) =< ((a ^ b) v (c ^ d))
37	36	leran 145	. . . . . 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 130	. . . . 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 82	. . . . . . . 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 34	. . . . . . 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 30	. . . . . . . . 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 73	. . . . . . . . . . . 12 ((c ^ d) v ((a ^ b) v (a ^ d))) = ((a ^ b) v ((c ^ d) v (a ^ d)))
43		ax-a3 31	. . . . . . . . . . . . 13 (((a ^ b) v (c ^ d)) v (a ^ d)) = ((a ^ b) v ((c ^ d) v (a ^ d)))
44	43	ax-r1 34	. . . . . . . . . . . 12 ((a ^ b) v ((c ^ d) v (a ^ d))) = (((a ^ b) v (c ^ d)) v (a ^ d))
45		ax-a2 30	. . . . . . . . . . . 12 (((a ^ b) v (c ^ d)) v (a ^ d)) = ((a ^ d) v ((a ^ b) v (c ^ d)))
46	42, 44, 45	3tr 62	. . . . . . . . . . 11 ((c ^ d) v ((a ^ b) v (a ^ d))) = ((a ^ d) v ((a ^ b) v (c ^ d)))
47	46	lor 66	. . . . . . . . . 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 31	. . . . . . . . . 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 31	. . . . . . . . . 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 60	. . . . . . . . 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 35	. . . . . . . 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 36	. . . . . . 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 85	. . . . . . . . . 10 (c_|_ v b_|_) = (c ^ b)_|_
54		oran3 85	. . . . . . . . . 10 (a_|_ v d_|_) = (a ^ d)_|_
55	53, 54	2an 72	. . . . . . . . 9 ((c_|_ v b_|_) ^ (a_|_ v d_|_)) = ((c ^ b)_|_ ^ (a ^ d)_|_)
56		anor3 82	. . . . . . . . 9 ((c ^ b)_|_ ^ (a ^ d)_|_) = ((c ^ b) v (a ^ d))_|_
57	55, 56	ax-r2 35	. . . . . . . 8 ((c_|_ v b_|_) ^ (a_|_ v d_|_)) = ((c ^ b) v (a ^ d))_|_
58	57	ran 71	. . . . . . 7 (((c_|_ v b_|_) ^ (a_|_ v d_|_)) ^ ((a ^ b) v (c ^ d))_|_) = (((c ^ b) v (a ^ d))_|_ ^ ((a ^ b) v (c ^ d))_|_)
59	40, 52, 58	3tr1 60	. . . . . 6 (((a ^ b) v (a ^ d)) v ((