d3oa - Quantum Logic Explorer

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

Theorem d3oa 995

Description: Derivation of 3-OA from OA distributive law. (Contributed by NM, 30-Dec-1998.)

**Hypothesis**
Ref	Expression
d3oa.1	f = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))

**Assertion**
Ref	Expression
d3oa	((a →₁c) ∩ f) ≤ (b →₁c)

**Proof of Theorem d3oa**
Step	Hyp	Ref	Expression
1		1oai1 821	. . 3 ((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)
2		2oath1i1 827	. . . 4 ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a →₁c) ∩ (b →₁c))
3		lear 161	. . . 4 ((a →₁c) ∩ (b →₁c)) ≤ (b →₁c)
4	2, 3	bltr 138	. . 3 ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)
5	1, 4	le2or 168	. 2 (((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ∪ ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) ≤ ((b →₁c) ∪ (b →₁c))
6		id 59	. . . . 5 (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c)))) = (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c))))
7		id 59	. . . . 5 (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c))))) = (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c)))))
8		leid 148	. . . . 5 (a →₁c) ≤ (a →₁c)
9		df-i1 44	. . . . . . 7 ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a ∩ b)^⊥ ∩ ((a →₁c) ∩ (b →₁c))))
10		ax-a1 30	. . . . . . . . . 10 (a ∩ b) = (a ∩ b)^⊥ ^⊥
11	10	ax-r1 35	. . . . . . . . 9 (a ∩ b)^⊥ ^⊥ = (a ∩ b)
12	11	bile 142	. . . . . . . 8 (a ∩ b)^⊥ ^⊥ ≤ (a ∩ b)
13		lear 161	. . . . . . . 8 ((a ∩ b)^⊥ ∩ ((a →₁c) ∩ (b →₁c))) ≤ ((a →₁c) ∩ (b →₁c))
14	12, 13	le2or 168	. . . . . . 7 ((a ∩ b)^⊥ ^⊥ ∪ ((a ∩ b)^⊥ ∩ ((a →₁c) ∩ (b →₁c)))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
15	9, 14	bltr 138	. . . . . 6 ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
16		leo 158	. . . . . 6 ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ≤ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c)))))
17	15, 16	letr 137	. . . . 5 ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ≤ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c)))))
18		df-i2 45	. . . . . . . 8 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ))
19		ax-a2 31	. . . . . . . 8 (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ )) = (((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ∪ ((a →₁c) ∩ (b →₁c)))
20	18, 19	ax-r2 36	. . . . . . 7 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) = (((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ∪ ((a →₁c) ∩ (b →₁c)))
21		lea 160	. . . . . . . . 9 ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ≤ (a ∩ b)^⊥ ^⊥
22	21, 11	lbtr 139	. . . . . . . 8 ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ≤ (a ∩ b)
23		leid 148	. . . . . . . 8 ((a →₁c) ∩ (b →₁c)) ≤ ((a →₁c) ∩ (b →₁c))
24	22, 23	le2or 168	. . . . . . 7 (((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ∪ ((a →₁c) ∩ (b →₁c))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
25	20, 24	bltr 138	. . . . . 6 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
26	25, 16	letr 137	. . . . 5 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) ≤ (((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) ∪ (((a ∩ a) ∪ ((a →₁c) ∩ (a →₁c))) ∩ ((b ∩ a) ∪ ((b →₁c) ∩ (a →₁c)))))
27		leo 158	. . . . . 6 ((a →₁c) ∩ (b →₁c)) ≤ (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ))
28	18	ax-r1 35	. . . . . 6 (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ )) = ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))
29	27, 28	lbtr 139	. . . . 5 ((a →₁c) ∩ (b →₁c)) ≤ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))
30	6, 7, 8, 17, 26, 29	ax-oadist 994	. . . 4 ((a →₁c) ∩ (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) = (((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ∪ ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))))
31	30	ax-r1 35	. . 3 (((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ∪ ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))))
32		u12lem 771	. . . . . . 7 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a ∩ b)^⊥ →₀((a →₁c) ∩ (b →₁c)))
33		df-i0 43	. . . . . . 7 ((a ∩ b)^⊥ →₀((a →₁c) ∩ (b →₁c))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
34	32, 33	ax-r2 36	. . . . . 6 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
35	10	ax-r5 38	. . . . . . 7 ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
36	35	ax-r1 35	. . . . . 6 ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
37	34, 36	ax-r2 36	. . . . 5 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
38		d3oa.1	. . . . . 6 f = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
39	38	ax-r1 35	. . . . 5 ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) = f
40	37, 39	ax-r2 36	. . . 4 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = f
41	40	lan 77	. . 3 ((a →₁c) ∩ (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ f)
42	31, 41	ax-r2 36	. 2 (((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ∪ ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ f)
43		oridm 110	. 2 ((b →₁c) ∪ (b →₁c)) = (b →₁c)
44	5, 42, 43	le3tr2 141	1 ((a →₁c) ∩ f) ≤ (b →₁c)

Colors of variables: term

Syntax hints: = wb 1 ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₀wi0 11 →₁wi1 12 →₂wi2 13

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 ax-oadist 994

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

This theorem is referenced by: d4oa 996

W3C validator