Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oa3to4lem6 930

Description: Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only.

**Hypotheses**
Ref	Expression
oa3to4lem6.oa4.1	a ≤ b^⊥
oa3to4lem6.oa4.2	c ≤ d^⊥
oa3to4lem6.3	g = ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))
oa3to4lem6.4	e = a^⊥
oa3to4lem6.5	f = c^⊥
oa3to4lem6.oa3	(e ∩ ((e →₁g) ∪ ((f →₁g) ∩ ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g)))))) ≤ ((e ∩ g) ∪ (f ∩ g))

**Assertion**
Ref	Expression
oa3to4lem6	((a ∪ b) ∩ (c ∪ d)) ≤ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))

**Proof of Theorem oa3to4lem6**
Step	Hyp	Ref	Expression
1		oa3to4lem6.oa4.1	. . . . . 6 a ≤ b^⊥
2	1	lecon3 149	. . . . 5 b ≤ a^⊥
3	2	lecon 146	. . . 4 a^⊥ ^⊥ ≤ b^⊥
4		oa3to4lem6.oa4.2	. . . . . 6 c ≤ d^⊥
5	4	lecon3 149	. . . . 5 d ≤ c^⊥
6	5	lecon 146	. . . 4 c^⊥ ^⊥ ≤ d^⊥
7		id 58	. . . 4 ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) = ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))
8		oa3to4lem6.oa3	. . . . 5 (e ∩ ((e →₁g) ∪ ((f →₁g) ∩ ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g)))))) ≤ ((e ∩ g) ∪ (f ∩ g))
9		oa3to4lem6.4	. . . . . 6 e = a^⊥
10		oa3to4lem6.3	. . . . . . . 8 g = ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))
11	9, 10	ud1lem0ab 249	. . . . . . 7 (e →₁g) = (a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
12		oa3to4lem6.5	. . . . . . . . 9 f = c^⊥
13	12, 10	ud1lem0ab 249	. . . . . . . 8 (f →₁g) = (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
14	9, 12	2an 72	. . . . . . . . 9 (e ∩ f) = (a^⊥ ∩ c^⊥ )
15	11, 13	2an 72	. . . . . . . . 9 ((e →₁g) ∩ (f →₁g)) = ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))
16	14, 15	2or 67	. . . . . . . 8 ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g))) = ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))))
17	13, 16	2an 72	. . . . . . 7 ((f →₁g) ∩ ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g)))) = ((c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))))
18	11, 17	2or 67	. . . . . 6 ((e →₁g) ∪ ((f →₁g) ∩ ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g))))) = ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∪ ((c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))))))
19	9, 18	2an 72	. . . . 5 (e ∩ ((e →₁g) ∪ ((f →₁g) ∩ ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g)))))) = (a^⊥ ∩ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∪ ((c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))))))
20	9, 10	2an 72	. . . . . 6 (e ∩ g) = (a^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
21	12, 10	2an 72	. . . . . 6 (f ∩ g) = (c^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
22	20, 21	2or 67	. . . . 5 ((e ∩ g) ∪ (f ∩ g)) = ((a^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∪ (c^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))
23	8, 19, 22	le3tr2 133	. . . 4 (a^⊥ ∩ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∪ ((c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))))))) ≤ ((a^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∪ (c^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))
24	3, 6, 7, 23	oa3to4lem4 928	. . 3 (a^⊥ ∩ (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))))) ≤ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))
25		anor3 82	. . . . . . . . . . 11 (a^⊥ ∩ c^⊥ ) = (a ∪ c)^⊥
26		anor3 82	. . . . . . . . . . 11 (b^⊥ ∩ d^⊥ ) = (b ∪ d)^⊥
27	25, 26	2or 67	. . . . . . . . . 10 ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )) = ((a ∪ c)^⊥ ∪ (b ∪ d)^⊥ )
28		oran3 85	. . . . . . . . . 10 ((a ∪ c)^⊥ ∪ (b ∪ d)^⊥ ) = ((a ∪ c) ∩ (b ∪ d))^⊥
29	27, 28	ax-r2 35	. . . . . . . . 9 ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )) = ((a ∪ c) ∩ (b ∪ d))^⊥
30	29	lan 70	. . . . . . . 8 (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))) = (d^⊥ ∩ ((a ∪ c) ∩ (b ∪ d))^⊥ )
31		anor3 82	. . . . . . . 8 (d^⊥ ∩ ((a ∪ c) ∩ (b ∪ d))^⊥ ) = (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥
32	30, 31	ax-r2 35	. . . . . . 7 (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))) = (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥
33	32	lor 66	. . . . . 6 (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )))) = (b^⊥ ∪ (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥ )
34		oran3 85	. . . . . 6 (b^⊥ ∪ (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥ ) = (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥
35	33, 34	ax-r2 35	. . . . 5 (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )))) = (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥
36	35	lan 70	. . . 4 (a^⊥ ∩ (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))))) = (a^⊥ ∩ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥ )
37		anor3 82	. . . 4 (a^⊥ ∩ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥ ) = (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))^⊥
38	36, 37	ax-r2 35	. . 3 (a^⊥ ∩ (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))))) = (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))^⊥
39		anor3 82	. . . . 5 (a^⊥ ∩ b^⊥ ) = (a ∪ b)^⊥
40		anor3 82	. . . . 5 (c^⊥ ∩ d^⊥ ) = (c ∪ d)^⊥
41	39, 40	2or 67	. . . 4 ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) = ((a ∪ b)^⊥ ∪ (c ∪ d)^⊥ )
42		oran3 85	. . . 4 ((a ∪ b)^⊥ ∪ (c ∪ d)^⊥ ) = ((a ∪ b) ∩ (c ∪ d))^⊥
43	41, 42	ax-r2 35	. . 3 ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) = ((a ∪ b) ∩ (c ∪ d))^⊥
44	24, 38, 43	le3tr2 133	. 2 (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))^⊥ ≤ ((a ∪ b) ∩ (c ∪ d))^⊥
45	44	lecon1 147	1 ((a ∪ b) ∩ (c ∪ d)) ≤ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))

Colors of variables: term

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

This theorem is referenced by: oa3to4 931

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