Theorem oa3-6lem 960

Description: Lemma for 3-OA(6). Equivalence with substitution into 4-OA.

Assertion

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

Proof of Theorem oa3-6lem

Step	Hyp	Ref	Expression
1		an1 98	. . . . . . . . 9 (a ^ 1) = a
2		1i1 266	. . . . . . . . . . 11 (1 ->1 c) = c
3	2	lan 70	. . . . . . . . . 10 ((a ->1 c) ^ (1 ->1 c)) = ((a ->1 c) ^ c)
4		u1lemab 592	. . . . . . . . . 10 ((a ->1 c) ^ c) = ((a ^ c) v (a_|_ ^ c))
5	3, 4	ax-r2 35	. . . . . . . . 9 ((a ->1 c) ^ (1 ->1 c)) = ((a ^ c) v (a_|_ ^ c))
6	1, 5	2or 67	. . . . . . . 8 ((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) = (a v ((a ^ c) v (a_|_ ^ c)))
7		ax-a3 31	. . . . . . . . 9 ((a v (a ^ c)) v (a_|_ ^ c)) = (a v ((a ^ c) v (a_|_ ^ c)))
8	7	ax-r1 34	. . . . . . . 8 (a v ((a ^ c) v (a_|_ ^ c))) = ((a v (a ^ c)) v (a_|_ ^ c))
9		a5b 112	. . . . . . . . 9 (a v (a ^ c)) = a
10	9	ax-r5 37	. . . . . . . 8 ((a v (a ^ c)) v (a_|_ ^ c)) = (a v (a_|_ ^ c))
11	6, 8, 10	3tr 62	. . . . . . 7 ((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) = (a v (a_|_ ^ c))
12		an1 98	. . . . . . . . 9 (b ^ 1) = b
13	2	lan 70	. . . . . . . . . 10 ((b ->1 c) ^ (1 ->1 c)) = ((b ->1 c) ^ c)
14		u1lemab 592	. . . . . . . . . 10 ((b ->1 c) ^ c) = ((b ^ c) v (b_|_ ^ c))
15	13, 14	ax-r2 35	. . . . . . . . 9 ((b ->1 c) ^ (1 ->1 c)) = ((b ^ c) v (b_|_ ^ c))
16	12, 15	2or 67	. . . . . . . 8 ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c))) = (b v ((b ^ c) v (b_|_ ^ c)))
17		ax-a3 31	. . . . . . . . 9 ((b v (b ^ c)) v (b_|_ ^ c)) = (b v ((b ^ c) v (b_|_ ^ c)))
18	17	ax-r1 34	. . . . . . . 8 (b v ((b ^ c) v (b_|_ ^ c))) = ((b v (b ^ c)) v (b_|_ ^ c))
19		a5b 112	. . . . . . . . 9 (b v (b ^ c)) = b
20	19	ax-r5 37	. . . . . . . 8 ((b v (b ^ c)) v (b_|_ ^ c)) = (b v (b_|_ ^ c))
21	16, 18, 20	3tr 62	. . . . . . 7 ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c))) = (b v (b_|_ ^ c))
22	11, 21	2an 72	. . . . . 6 (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c)))) = ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))
23	22	lor 66	. . . . 5 (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c))))) = (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c))))
24		or32 75	. . . . 5 (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))) = (((a ^ b) v ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))) v ((a ->1 c) ^ (b ->1 c)))
25		leo 150	. . . . . . . . 9 a =< (a v (a_|_ ^ c))
26		leo 150	. . . . . . . . 9 b =< (b v (b_|_ ^ c))
27	25, 26	le2an 161	. . . . . . . 8 (a ^ b) =< ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))
28	27	df-le2 123	. . . . . . 7 ((a ^ b) v ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))) = ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))
29		ax-a1 29	. . . . . . . . . 10 a = a_|__|_
30	29	ax-r5 37	. . . . . . . . 9 (a v (a_|_ ^ c)) = (a_|__|_ v (a_|_ ^ c))
31		df-i1 43	. . . . . . . . . 10 (a_|_ ->1 c) = (a_|__|_ v (a_|_ ^ c))
32	31	ax-r1 34	. . . . . . . . 9 (a_|__|_ v (a_|_ ^ c)) = (a_|_ ->1 c)
33	30, 32	ax-r2 35	. . . . . . . 8 (a v (a_|_ ^ c)) = (a_|_ ->1 c)
34		ax-a1 29	. . . . . . . . . 10 b = b_|__|_
35	34	ax-r5 37	. . . . . . . . 9 (b v (b_|_ ^ c)) = (b_|__|_ v (b_|_ ^ c))
36		df-i1 43	. . . . . . . . . 10 (b_|_ ->1 c) = (b_|__|_ v (b_|_ ^ c))
37	36	ax-r1 34	. . . . . . . . 9 (b_|__|_ v (b_|_ ^ c)) = (b_|_ ->1 c)
38	35, 37	ax-r2 35	. . . . . . . 8 (b v (b_|_ ^ c)) = (b_|_ ->1 c)
39	33, 38	2an 72	. . . . . . 7 ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c))) = ((a_|_ ->1 c) ^ (b_|_ ->1 c))
40	28, 39	ax-r2 35	. . . . . 6 ((a ^ b) v ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))) = ((a_|_ ->1 c) ^ (b_|_ ->1 c))
41	40	ax-r5 37	. . . . 5 (((a ^ b) v ((a v (a_|_ ^ c)) ^ (b v (b_|_ ^ c)))) v ((a ->1 c) ^ (b ->1 c))) = (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))
42	23, 24, 41	3tr 62	. . . 4 (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c))))) = (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))
43	42	lan 70	. . 3 (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c)))))) = (b ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))
44	43	lor 66	. 2 (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c))))))) = (a v (b ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))
45	44	lan 70	1 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c)))))))) = ((a ->1 c) ^ (a v (b ^ (((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-6to3 967

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