Theorem oa6to4 938

Description: Derivation of 4-variable proper OA law, assuming 6-variable OA law.

Hypotheses

Ref	Expression
oa6to4.1	b_|_ = (a ->1 g)_|_
oa6to4.2	d_|_ = (c ->1 g)_|_
oa6to4.3	f_|_ = (e ->1 g)_|_
oa6to4.oa6	(((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_|_)))))))

Assertion

Ref	Expression
oa6to4	((a ->1 g) ^ (a v (c ^ (((a ^ c) v ((a ->1 g) ^ (c ->1 g))) v (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g)))))))) =< (((a ^ g) v (c ^ g)) v (e ^ g))

Proof of Theorem oa6to4

Step	Hyp	Ref	Expression
1		oa6to4.oa6	. . 3 (((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_|_)))))))
2	1	oa6todual 932	. 2 (b ^ (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))))))) =< (((a ^ b) v (c ^ d)) v (e ^ f))
3		oa6to4.1	. . . 4 b_|_ = (a ->1 g)_|_
4	3	con1 63	. . 3 b = (a ->1 g)
5		oa6to4.2	. . . . . . . . 9 d_|_ = (c ->1 g)_|_
6	5	con1 63	. . . . . . . 8 d = (c ->1 g)
7	4, 6	2an 72	. . . . . . 7 (b ^ d) = ((a ->1 g) ^ (c ->1 g))
8	7	lor 66	. . . . . 6 ((a ^ c) v (b ^ d)) = ((a ^ c) v ((a ->1 g) ^ (c ->1 g)))
9		oa6to4.3	. . . . . . . . . 10 f_|_ = (e ->1 g)_|_
10	9	con1 63	. . . . . . . . 9 f = (e ->1 g)
11	4, 10	2an 72	. . . . . . . 8 (b ^ f) = ((a ->1 g) ^ (e ->1 g))
12	11	lor 66	. . . . . . 7 ((a ^ e) v (b ^ f)) = ((a ^ e) v ((a ->1 g) ^ (e ->1 g)))
13	6, 10	2an 72	. . . . . . . 8 (d ^ f) = ((c ->1 g) ^ (e ->1 g))
14	13	lor 66	. . . . . . 7 ((c ^ e) v (d ^ f)) = ((c ^ e) v ((c ->1 g) ^ (e ->1 g)))
15	12, 14	2an 72	. . . . . 6 (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))) = (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g))))
16	8, 15	2or 67	. . . . 5 (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))) = (((a ^ c) v ((a ->1 g) ^ (c ->1 g))) v (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g)))))
17	16	lan 70	. . . 4 (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))))) = (c ^ (((a ^ c) v ((a ->1 g) ^ (c ->1 g))) v (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g))))))
18	17	lor 66	. . 3 (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))))) = (a v (c ^ (((a ^ c) v ((a ->1 g) ^ (c ->1 g))) v (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g)))))))
19	4, 18	2an 72	. 2 (b ^ (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))))))) = ((a ->1 g) ^ (a v (c ^ (((a ^ c) v ((a ->1 g) ^ (c ->1 g))) v (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g))))))))
20	4	lan 70	. . . . 5 (a ^ b) = (a ^ (a ->1 g))
21		ancom 68	. . . . 5 (a ^ (a ->1 g)) = ((a ->1 g) ^ a)
22		u1lemaa 582	. . . . 5 ((a ->1 g) ^ a) = (a ^ g)
23	20, 21, 22	3tr 62	. . . 4 (a ^ b) = (a ^ g)
24	6	lan 70	. . . . 5 (c ^ d) = (c ^ (c ->1 g))
25		ancom 68	. . . . 5 (c ^ (c ->1 g)) = ((c ->1 g) ^ c)
26		u1lemaa 582	. . . . 5 ((c ->1 g) ^ c) = (c ^ g)
27	24, 25, 26	3tr 62	. . . 4 (c ^ d) = (c ^ g)
28	23, 27	2or 67	. . 3 ((a ^ b) v (c ^ d)) = ((a ^ g) v (c ^ g))
29	10	lan 70	. . . 4 (e ^ f) = (e ^ (e ->1 g))
30		ancom 68	. . . 4 (e ^ (e ->1 g)) = ((e ->1 g) ^ e)
31		u1lemaa 582	. . . 4 ((e ->1 g) ^ e) = (e ^ g)
32	29, 30, 31	3tr 62	. . 3 (e ^ f) = (e ^ g)
33	28, 32	2or 67	. 2 (((a ^ b) v (c ^ d)) v (e ^ f)) = (((a ^ g) v (c ^ g)) v (e ^ g))
34	2, 19, 33	le3tr2 133	1 ((a ->1 g) ^ (a v (c ^ (((a ^ c) v ((a ->1 g) ^ (c ->1 g))) v (((a ^ e) v ((a ->1 g) ^ (e ->1 g))) ^ ((c ^ e) v ((c ->1 g) ^ (e ->1 g)))))))) =< (((a ^ g) v (c ^ g)) v (e ^ g))

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13

This theorem is referenced by:  oa3-2to2s 970  axoa4a 1016

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-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org