Theorem oa4to6 945

Description: Orthoarguesian law (4-variable to 6-variable proof). The first 3 hypotheses are those for 6-OA. The next 4 are variable substitutions into 4-OA. The last is the 4-OA. The proof uses OM logic only.

Hypotheses

Ref	Expression
oa4to6.oa6.1	a =< b_|_
oa4to6.oa6.2	c =< d_|_
oa4to6.oa6.3	e =< f_|_
oa4to6.4	g = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))
oa4to6.5	h = a_|_
oa4to6.6	j = c_|_
oa4to6.7	k = e_|_
oa4to6.oa4	((h ->1 g) ^ (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))))) =< g

Assertion

Ref	Expression
oa4to6	(((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))

Proof of Theorem oa4to6

Step	Hyp	Ref	Expression
1		oa4to6.oa6.1	. . . . 5 a =< b_|_
2	1	lecon3 149	. . . 4 b =< a_|_
3	2	lecon 146	. . 3 a_|__|_ =< b_|_
4		oa4to6.oa6.2	. . . . 5 c =< d_|_
5	4	lecon3 149	. . . 4 d =< c_|_
6	5	lecon 146	. . 3 c_|__|_ =< d_|_
7		oa4to6.oa6.3	. . . . 5 e =< f_|_
8	7	lecon3 149	. . . 4 f =< e_|_
9	8	lecon 146	. . 3 e_|__|_ =< f_|_
10		id 58	. . 3 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)) = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))
11		oa4to6.oa4	. . . 4 ((h ->1 g) ^ (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))))) =< g
12		oa4to6.5	. . . . . 6 h = a_|_
13		oa4to6.4	. . . . . 6 g = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))
14	12, 13	ud1lem0ab 249	. . . . 5 (h ->1 g) = (a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))
15		oa4to6.6	. . . . . . 7 j = c_|_
16	12, 15	2an 72	. . . . . . . . 9 (h ^ j) = (a_|_ ^ c_|_)
17	15, 13	ud1lem0ab 249	. . . . . . . . . 10 (j ->1 g) = (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))
18	14, 17	2an 72	. . . . . . . . 9 ((h ->1 g) ^ (j ->1 g)) = ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))
19	16, 18	2or 67	. . . . . . . 8 ((h ^ j) v ((h ->1 g) ^ (j ->1 g))) = ((a_|_ ^ c_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))
20		oa4to6.7	. . . . . . . . . . 11 k = e_|_
21	12, 20	2an 72	. . . . . . . . . 10 (h ^ k) = (a_|_ ^ e_|_)
22	20, 13	ud1lem0ab 249	. . . . . . . . . . 11 (k ->1 g) = (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))
23	14, 22	2an 72	. . . . . . . . . 10 ((h ->1 g) ^ (k ->1 g)) = ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))
24	21, 23	2or 67	. . . . . . . . 9 ((h ^ k) v ((h ->1 g) ^ (k ->1 g))) = ((a_|_ ^ e_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))
25	15, 20	2an 72	. . . . . . . . . 10 (j ^ k) = (c_|_ ^ e_|_)
26	17, 22	2an 72	. . . . . . . . . 10 ((j ->1 g) ^ (k ->1 g)) = ((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))
27	25, 26	2or 67	. . . . . . . . 9 ((j ^ k) v ((j ->1 g) ^ (k ->1 g))) = ((c_|_ ^ e_|_) v ((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))
28	24, 27	2an 72	. . . . . . . 8 (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))) = (((a_|_ ^ e_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) ^ ((c_|_ ^ e_|_) v ((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))))
29	19, 28	2or 67	. . . . . . 7 (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g))))) = (((a_|_ ^ c_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) v (((a_|_ ^ e_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) ^ ((c_|_ ^ e_|_) v ((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_)))))))
30	15, 29	2an 72	. . . . . 6 (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g)))))) = (c_|_ ^ (((a_|_ ^ c_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) v (((a_|_ ^ e_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) ^ ((c_|_ ^ e_|_) v ((c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))))))
31	12, 30	2or 67	. . . . 5 (h v (j ^ (((h ^ j) v ((h ->1 g) ^ (j ->1 g))) v (((h ^ k) v ((h ->1 g) ^ (k ->1 g))) ^ ((j ^ k) v ((j ->1 g) ^ (k ->1 g))))))) = (a_|_ v (c_|_ ^ (((a_|_ ^ c_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (c_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))))) v (((a_|_ ^ e_|_) v ((a_|_ ->1 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))) ^ (e_|_ ->1 (((a