Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

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^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))
oa4to6.5	h = a^⊥
oa4to6.6	j = c^⊥
oa4to6.7	k = e^⊥
oa4to6.oa4	((h →₁g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) ∪ (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g)))))))) ≤ g

**Assertion**
Ref	Expression
oa4to6	(((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ 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^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )) = (((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))
11		oa4to6.oa4	. . . 4 ((h →₁g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) ∪ (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g)))))))) ≤ g
12		oa4to6.5	. . . . . 6 h = a^⊥
13		oa4to6.4	. . . . . 6 g = (((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))
14	12, 13	ud1lem0ab 249	. . . . 5 (h →₁g) = (a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (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 →₁g) = (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))
18	14, 17	2an 72	. . . . . . . . 9 ((h →₁g) ∩ (j →₁g)) = ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))
19	16, 18	2or 67	. . . . . . . 8 ((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) = ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (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 →₁g) = (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))
23	14, 22	2an 72	. . . . . . . . . 10 ((h →₁g) ∩ (k →₁g)) = ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))
24	21, 23	2or 67	. . . . . . . . 9 ((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) = ((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))))
25	15, 20	2an 72	. . . . . . . . . 10 (j ∩ k) = (c^⊥ ∩ e^⊥ )
26	17, 22	2an 72	. . . . . . . . . 10 ((j →₁g) ∩ (k →₁g)) = ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))
27	25, 26	2or 67	. . . . . . . . 9 ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g))) = ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))))
28	24, 27	2an 72	. . . . . . . 8 (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g)))) = (((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∩ ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))))
29	19, 28	2or 67	. . . . . . 7 (((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) ∪ (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g))))) = (((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∪ (((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∩ ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))))))
30	15, 29	2an 72	. . . . . 6 (j ∩ (((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) ∪ (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g)))))) = (c^⊥ ∩ (((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∪ (((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∩ ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))))))
31	12, 30	2or 67	. . . . 5 (h ∪ (j ∩ (((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) ∪ (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g))))))) = (a^⊥ ∪ (c^⊥ ∩ (((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∪ (((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∩ ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))))))))
32	14, 31	2an 72	. . . 4 ((h →₁g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →₁g) ∩ (j →₁g))) ∪ (((h ∩ k) ∪ ((h →₁g) ∩ (k →₁g))) ∩ ((j ∩ k) ∪ ((j →₁g) ∩ (k →₁g)))))))) = ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (a^⊥ ∪ (c^⊥ ∩ (((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∪ (((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∩ ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))))))))
33	11, 32, 13	le3tr2 133	. . 3 ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (a^⊥ ∪ (c^⊥ ∩ (((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∪ (((a^⊥ ∩ e^⊥ ) ∪ ((a^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))))) ∩ ((c^⊥ ∩ e^⊥ ) ∪ ((c^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))) ∩ (e^⊥ →₁(((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ )))))))))) ≤ (((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))
34	3, 6, 9, 10, 33	oa4to6dual 944	. 2 (b^⊥ ∩ (a^⊥ ∪ (c^⊥ ∩ (((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )) ∪ (((a^⊥ ∩ e^⊥ ) ∪ (b^⊥ ∩ f^⊥ )) ∩ ((c^⊥ ∩ e^⊥ ) ∪ (d^⊥ ∩ f^⊥ ))))))) ≤ (((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) ∪ (e^⊥ ∩ f^⊥ ))
35	34	oa6fromdual 933	1 (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))

Colors of variables: term

Syntax hints: = wb 1 ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₁wi1 13

This theorem is referenced by: oa3-2to2s 970 d6oa 977 oa6 1015

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