oa3to4lem6 - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > oa3to4lem6		GIF version

Theorem oa3to4lem6 950

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. (Contributed by NM, 19-Dec-1998.)

**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 157	. . . . 5 b ≤ a^⊥
3	2	lecon 154	. . . 4 a^⊥ ^⊥ ≤ b^⊥
4		oa3to4lem6.oa4.2	. . . . . 6 c ≤ d^⊥
5	4	lecon3 157	. . . . 5 d ≤ c^⊥
6	5	lecon 154	. . . 4 c^⊥ ^⊥ ≤ d^⊥
7		id 59	. . . 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 257	. . . . . . 7 (e →₁g) = (a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
12		oa3to4lem6.5	. . . . . . . . 9 f = c^⊥
13	12, 10	ud1lem0ab 257	. . . . . . . 8 (f →₁g) = (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
14	9, 12	2an 79	. . . . . . . . 9 (e ∩ f) = (a^⊥ ∩ c^⊥ )
15	11, 13	2an 79	. . . . . . . . 9 ((e →₁g) ∩ (f →₁g)) = ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))
16	14, 15	2or 72	. . . . . . . 8 ((e ∩ f) ∪ ((e →₁g) ∩ (f →₁g))) = ((a^⊥ ∩ c^⊥ ) ∪ ((a^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∩ (c^⊥ →₁((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))))
17	13, 16	2an 79	. . . . . . 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 72	. . . . . 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 79	. . . . 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 79	. . . . . 6 (e ∩ g) = (a^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
21	12, 10	2an 79	. . . . . 6 (f ∩ g) = (c^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )))
22	20, 21	2or 72	. . . . 5 ((e ∩ g) ∪ (f ∩ g)) = ((a^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))) ∪ (c^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))))
23	8, 19, 22	le3tr2 141	. . . 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 948	. . 3 (a^⊥ ∩ (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))))) ≤ ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ ))
25		anor3 90	. . . . . . . . . . 11 (a^⊥ ∩ c^⊥ ) = (a ∪ c)^⊥
26		anor3 90	. . . . . . . . . . 11 (b^⊥ ∩ d^⊥ ) = (b ∪ d)^⊥
27	25, 26	2or 72	. . . . . . . . . 10 ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )) = ((a ∪ c)^⊥ ∪ (b ∪ d)^⊥ )
28		oran3 93	. . . . . . . . . 10 ((a ∪ c)^⊥ ∪ (b ∪ d)^⊥ ) = ((a ∪ c) ∩ (b ∪ d))^⊥
29	27, 28	ax-r2 36	. . . . . . . . 9 ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )) = ((a ∪ c) ∩ (b ∪ d))^⊥
30	29	lan 77	. . . . . . . 8 (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))) = (d^⊥ ∩ ((a ∪ c) ∩ (b ∪ d))^⊥ )
31		anor3 90	. . . . . . . 8 (d^⊥ ∩ ((a ∪ c) ∩ (b ∪ d))^⊥ ) = (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥
32	30, 31	ax-r2 36	. . . . . . 7 (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))) = (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥
33	32	lor 70	. . . . . 6 (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )))) = (b^⊥ ∪ (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥ )
34		oran3 93	. . . . . 6 (b^⊥ ∪ (d ∪ ((a ∪ c) ∩ (b ∪ d)))^⊥ ) = (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥
35	33, 34	ax-r2 36	. . . . 5 (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ )))) = (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥
36	35	lan 77	. . . 4 (a^⊥ ∩ (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))))) = (a^⊥ ∩ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥ )
37		anor3 90	. . . 4 (a^⊥ ∩ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))^⊥ ) = (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))^⊥
38	36, 37	ax-r2 36	. . 3 (a^⊥ ∩ (b^⊥ ∪ (d^⊥ ∩ ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ d^⊥ ))))) = (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))^⊥
39		anor3 90	. . . . 5 (a^⊥ ∩ b^⊥ ) = (a ∪ b)^⊥
40		anor3 90	. . . . 5 (c^⊥ ∩ d^⊥ ) = (c ∪ d)^⊥
41	39, 40	2or 72	. . . 4 ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) = ((a ∪ b)^⊥ ∪ (c ∪ d)^⊥ )
42		oran3 93	. . . 4 ((a ∪ b)^⊥ ∪ (c ∪ d)^⊥ ) = ((a ∪ b) ∩ (c ∪ d))^⊥
43	41, 42	ax-r2 36	. . 3 ((a^⊥ ∩ b^⊥ ) ∪ (c^⊥ ∩ d^⊥ )) = ((a ∪ b) ∩ (c ∪ d))^⊥
44	24, 38, 43	le3tr2 141	. 2 (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))^⊥ ≤ ((a ∪ b) ∩ (c ∪ d))^⊥
45	44	lecon1 155	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 12

This theorem was proved from 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 theorem 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 referenced by: oa3to4 951

W3C validator