Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem d3oa 975

Description: Derivation of 3-OA from OA distributive law.

**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 803	. . 3 ((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)
2		2oath1i1 809	. . . 4 ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a →₁c) ∩ (b →₁c))
3		lear 153	. . . 4 ((a →₁c) ∩ (b →₁c)) ≤ (b →₁c)
4	2, 3	bltr 130	. . 3 ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)
5	1, 4	le2or 160	. 2 (((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ∪ ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) ≤ ((b →₁c) ∪ (b →₁c))
6		id 58	. . . . 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 58	. . . . 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 140	. . . . 5 (a →₁c) ≤ (a →₁c)
9		df-i1 43	. . . . . . 7 ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a ∩ b)^⊥ ∩ ((a →₁c) ∩ (b →₁c))))
10		ax-a1 29	. . . . . . . . . 10 (a ∩ b) = (a ∩ b)^⊥ ^⊥
11	10	ax-r1 34	. . . . . . . . 9 (a ∩ b)^⊥ ^⊥ = (a ∩ b)
12	11	bile 134	. . . . . . . 8 (a ∩ b)^⊥ ^⊥ ≤ (a ∩ b)
13		lear 153	. . . . . . . 8 ((a ∩ b)^⊥ ∩ ((a →₁c) ∩ (b →₁c))) ≤ ((a →₁c) ∩ (b →₁c))
14	12, 13	le2or 160	. . . . . . 7 ((a ∩ b)^⊥ ^⊥ ∪ ((a ∩ b)^⊥ ∩ ((a →₁c) ∩ (b →₁c)))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
15	9, 14	bltr 130	. . . . . 6 ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
16		leo 150	. . . . . 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 129	. . . . 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 44	. . . . . . . 8 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ))
19		ax-a2 30	. . . . . . . 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 35	. . . . . . 7 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) = (((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ∪ ((a →₁c) ∩ (b →₁c)))
21		lea 152	. . . . . . . . 9 ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ≤ (a ∩ b)^⊥ ^⊥
22	21, 11	lbtr 131	. . . . . . . 8 ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ≤ (a ∩ b)
23		leid 140	. . . . . . . 8 ((a →₁c) ∩ (b →₁c)) ≤ ((a →₁c) ∩ (b →₁c))
24	22, 23	le2or 160	. . . . . . 7 (((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ) ∪ ((a →₁c) ∩ (b →₁c))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
25	20, 24	bltr 130	. . . . . 6 ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))) ≤ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
26	25, 16	letr 129	. . . . 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 150	. . . . . 6 ((a →₁c) ∩ (b →₁c)) ≤ (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ ))
28	18	ax-r1 34	. . . . . 6 (((a →₁c) ∩ (b →₁c)) ∪ ((a ∩ b)^⊥ ^⊥ ∩ ((a →₁c) ∩ (b →₁c))^⊥ )) = ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))
29	27, 28	lbtr 131	. . . . 5 ((a →₁c) ∩ (b →₁c)) ≤ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))
30	6, 7, 8, 17, 26, 29	ax-oadist 974	. . . 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 34	. . 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 753	. . . . . . 7 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a ∩ b)^⊥ →₀((a →₁c) ∩ (b →₁c)))
33		df-i0 42	. . . . . . 7 ((a ∩ b)^⊥ →₀((a →₁c) ∩ (b →₁c))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
34	32, 33	ax-r2 35	. . . . . 6 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
35	10	ax-r5 37	. . . . . . 7 ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) = ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
36	35	ax-r1 34	. . . . . 6 ((a ∩ b)^⊥ ^⊥ ∪ ((a →₁c) ∩ (b →₁c))) = ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
37	34, 36	ax-r2 35	. . . . 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 34	. . . . 5 ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))) = f
40	37, 39	ax-r2 35	. . . 4 (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c)))) = f
41	40	lan 70	. . 3 ((a →₁c) ∩ (((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c))) ∪ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ f)
42	31, 41	ax-r2 35	. 2 (((a →₁c) ∩ ((a ∩ b)^⊥ →₁((a →₁c) ∩ (b →₁c)))) ∪ ((a →₁c) ∩ ((a ∩ b)^⊥ →₂((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ f)
43		oridm 102	. 2 ((b →₁c) ∪ (b →₁c)) = (b →₁c)
44	5, 42, 43	le3tr2 133	1 ((a →₁c) ∩ f) ≤ (b →₁c)

Colors of variables: term

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

This theorem is referenced by: d4oa 976

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

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i0 42 df-i1 43 df-i2 44 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org