Theorem oa6to4 958

Description: Derivation of 4-variable proper OA law, assuming 6-variable OA law. (Contributed by NM, 22-Dec-1998.)

Hypotheses

Ref	Expression
oa6to4.1	b⊥ = (a →1 g)⊥
oa6to4.2	d⊥ = (c →1 g)⊥
oa6to4.3	f⊥ = (e →1 g)⊥
oa6to4.oa6	(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))

Assertion

Ref	Expression
oa6to4	((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))

Proof of Theorem oa6to4

Step	Hyp	Ref	Expression
1		oa6to4.oa6	. . 3 (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))
2	1	oa6todual 952	. 2 (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))
3		oa6to4.1	. . . 4 b⊥ = (a →1 g)⊥
4	3	con1 66	. . 3 b = (a →1 g)
5		oa6to4.2	. . . . . . . . 9 d⊥ = (c →1 g)⊥
6	5	con1 66	. . . . . . . 8 d = (c →1 g)
7	4, 6	2an 79	. . . . . . 7 (b ∩ d) = ((a →1 g) ∩ (c →1 g))
8	7	lor 70	. . . . . 6 ((a ∩ c) ∪ (b ∩ d)) = ((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g)))
9		oa6to4.3	. . . . . . . . . 10 f⊥ = (e →1 g)⊥
10	9	con1 66	. . . . . . . . 9 f = (e →1 g)
11	4, 10	2an 79	. . . . . . . 8 (b ∩ f) = ((a →1 g) ∩ (e →1 g))
12	11	lor 70	. . . . . . 7 ((a ∩ e) ∪ (b ∩ f)) = ((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g)))
13	6, 10	2an 79	. . . . . . . 8 (d ∩ f) = ((c →1 g) ∩ (e →1 g))
14	13	lor 70	. . . . . . 7 ((c ∩ e) ∪ (d ∩ f)) = ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))
15	12, 14	2an 79	. . . . . 6 (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))) = (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g))))
16	8, 15	2or 72	. . . . 5 (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))) = (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))
17	16	lan 77	. . . 4 (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))) = (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g))))))
18	17	lor 70	. . 3 (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))))) = (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))
19	4, 18	2an 79	. 2 (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) = ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g))))))))
20	4	lan 77	. . . . 5 (a ∩ b) = (a ∩ (a →1 g))
21		ancom 74	. . . . 5 (a ∩ (a →1 g)) = ((a →1 g) ∩ a)
22		u1lemaa 600	. . . . 5 ((a →1 g) ∩ a) = (a ∩ g)
23	20, 21, 22	3tr 65	. . . 4 (a ∩ b) = (a ∩ g)
24	6	lan 77	. . . . 5 (c ∩ d) = (c ∩ (c →1 g))
25		ancom 74	. . . . 5 (c ∩ (c →1 g)) = ((c →1 g) ∩ c)
26		u1lemaa 600	. . . . 5 ((c →1 g) ∩ c) = (c ∩ g)
27	24, 25, 26	3tr 65	. . . 4 (c ∩ d) = (c ∩ g)
28	23, 27	2or 72	. . 3 ((a ∩ b) ∪ (c ∩ d)) = ((a ∩ g) ∪ (c ∩ g))
29	10	lan 77	. . . 4 (e ∩ f) = (e ∩ (e →1 g))
30		ancom 74	. . . 4 (e ∩ (e →1 g)) = ((e →1 g) ∩ e)
31		u1lemaa 600	. . . 4 ((e →1 g) ∩ e) = (e ∩ g)
32	29, 30, 31	3tr 65	. . 3 (e ∩ f) = (e ∩ g)
33	28, 32	2or 72	. 2 (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f)) = (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))
34	2, 19, 33	le3tr2 141	1 ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₁ wi1 12

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  oa3-2to2s  990  axoa4a  1037