Theorem oa3-u1lem 965

Description: Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual.

Assertion

Ref	Expression
oa3-u1lem	(1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = (c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))))

Proof of Theorem oa3-u1lem

Step	Hyp	Ref	Expression
1		ancom 68	. 2 (1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = ((c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))) ^ 1)
2		an1 98	. 2 ((c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))) ^ 1) = (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))
3		lea 152	. . . . . . . . 9 (a_|_ ^ c) =< a_|_
4		leo 150	. . . . . . . . 9 a_|_ =< (a_|_ v (a ^ c))
5	3, 4	letr 129	. . . . . . . 8 (a_|_ ^ c) =< (a_|_ v (a ^ c))
6		leor 151	. . . . . . . 8 (a ^ c) =< (a_|_ v (a ^ c))
7	5, 6	lel2or 162	. . . . . . 7 ((a_|_ ^ c) v (a ^ c)) =< (a_|_ v (a ^ c))
8	7	df-le2 123	. . . . . 6 (((a_|_ ^ c) v (a ^ c)) v (a_|_ v (a ^ c))) = (a_|_ v (a ^ c))
9		ancom 68	. . . . . . . 8 (c ^ (a_|_ ->1 c)) = ((a_|_ ->1 c) ^ c)
10		u1lemab 592	. . . . . . . 8 ((a_|_ ->1 c) ^ c) = ((a_|_ ^ c) v (a_|__|_ ^ c))
11		ax-a1 29	. . . . . . . . . . 11 a = a_|__|_
12	11	ax-r1 34	. . . . . . . . . 10 a_|__|_ = a
13	12	ran 71	. . . . . . . . 9 (a_|__|_ ^ c) = (a ^ c)
14	13	lor 66	. . . . . . . 8 ((a_|_ ^ c) v (a_|__|_ ^ c)) = ((a_|_ ^ c) v (a ^ c))
15	9, 10, 14	3tr 62	. . . . . . 7 (c ^ (a_|_ ->1 c)) = ((a_|_ ^ c) v (a ^ c))
16		ancom 68	. . . . . . . 8 (1 ^ (a ->1 c)) = ((a ->1 c) ^ 1)
17		an1 98	. . . . . . . 8 ((a ->1 c) ^ 1) = (a ->1 c)
18		df-i1 43	. . . . . . . 8 (a ->1 c) = (a_|_ v (a ^ c))
19	16, 17, 18	3tr 62	. . . . . . 7 (1 ^ (a ->1 c)) = (a_|_ v (a ^ c))
20	15, 19	2or 67	. . . . . 6 ((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) = (((a_|_ ^ c) v (a ^ c)) v (a_|_ v (a ^ c)))
21	8, 20, 18	3tr1 60	. . . . 5 ((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) = (a ->1 c)
22		lea 152	. . . . . . . . . 10 (b_|_ ^ c) =< b_|_
23		leo 150	. . . . . . . . . 10 b_|_ =< (b_|_ v (b ^ c))
24	22, 23	letr 129	. . . . . . . . 9 (b_|_ ^ c) =< (b_|_ v (b ^ c))
25		leor 151	. . . . . . . . 9 (b ^ c) =< (b_|_ v (b ^ c))
26	24, 25	lel2or 162	. . . . . . . 8 ((b_|_ ^ c) v (b ^ c)) =< (b_|_ v (b ^ c))
27	26	df-le2 123	. . . . . . 7 (((b_|_ ^ c) v (b ^ c)) v (b_|_ v (b ^ c))) = (b_|_ v (b ^ c))
28		ancom 68	. . . . . . . . 9 (c ^ (b_|_ ->1 c)) = ((b_|_ ->1 c) ^ c)
29		u1lemab 592	. . . . . . . . 9 ((b_|_ ->1 c) ^ c) = ((b_|_ ^ c) v (b_|__|_ ^ c))
30		ax-a1 29	. . . . . . . . . . . 12 b = b_|__|_
31	30	ax-r1 34	. . . . . . . . . . 11 b_|__|_ = b
32	31	ran 71	. . . . . . . . . 10 (b_|__|_ ^ c) = (b ^ c)
33	32	lor 66	. . . . . . . . 9 ((b_|_ ^ c) v (b_|__|_ ^ c)) = ((b_|_ ^ c) v (b ^ c))
34	28, 29, 33	3tr 62	. . . . . . . 8 (c ^ (b_|_ ->1 c)) = ((b_|_ ^ c) v (b ^ c))
35		ancom 68	. . . . . . . . 9 (1 ^ (b ->1 c)) = ((b ->1 c) ^ 1)
36		an1 98	. . . . . . . . 9 ((b ->1 c) ^ 1) = (b ->1 c)
37		df-i1 43	. . . . . . . . 9 (b ->1 c) = (b_|_ v (b ^ c))
38	35, 36, 37	3tr 62	. . . . . . . 8 (1 ^ (b ->1 c)) = (b_|_ v (b ^ c))
39	34, 38	2or 67	. . . . . . 7 ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) = (((b_|_ ^ c) v (b ^ c)) v (b_|_ v (b ^ c)))
40	27, 39, 37	3tr1 60	. . . . . 6 ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) = (b ->1 c)
41		ax-a2 30	. . . . . 6 (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) = (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))
42	40, 41	2an 72	. . . . 5 (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))) = ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))
43	21, 42	2or 67	. . . 4 (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))
44	43	lan 70	. . 3 ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))) = ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))
45	44	lor 66	. 2 (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))) = (c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))))
46	1, 2, 45	3tr 62	1 (1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = (c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))))

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

This theorem is referenced by:  oa3-u1 971

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