oaidlem2 - Quantum Logic Explorer

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

Theorem oaidlem2 931

Description: Lemma for identity-like OA law. (Contributed by NM, 22-Jan-1999.)

**Hypothesis**
Ref	Expression
oaidlem2.1	((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c) →₁(b →₁c))) = 1

**Assertion**
Ref	Expression
oaidlem2	((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)

**Proof of Theorem oaidlem2**
Step	Hyp	Ref	Expression
1		anidm 111	. . . . . . . . . 10 ((a →₁c) ∩ (a →₁c)) = (a →₁c)
2	1	ax-r1 35	. . . . . . . . 9 (a →₁c) = ((a →₁c) ∩ (a →₁c))
3	2	ran 78	. . . . . . . 8 ((a →₁c) ∩ (b →₁c)) = (((a →₁c) ∩ (a →₁c)) ∩ (b →₁c))
4		anass 76	. . . . . . . 8 (((a →₁c) ∩ (a →₁c)) ∩ (b →₁c)) = ((a →₁c) ∩ ((a →₁c) ∩ (b →₁c)))
5	3, 4	ax-r2 36	. . . . . . 7 ((a →₁c) ∩ (b →₁c)) = ((a →₁c) ∩ ((a →₁c) ∩ (b →₁c)))
6		leor 159	. . . . . . . 8 ((a →₁c) ∩ (b →₁c)) ≤ (d ∪ ((a →₁c) ∩ (b →₁c)))
7	6	lelan 167	. . . . . . 7 ((a →₁c) ∩ ((a →₁c) ∩ (b →₁c))) ≤ ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
8	5, 7	bltr 138	. . . . . 6 ((a →₁c) ∩ (b →₁c)) ≤ ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
9	8	df-le2 131	. . . . 5 (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
10		ax-a3 32	. . . . . 6 (((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ (a →₁c)^⊥ ) ∪ ((a →₁c) ∩ (b →₁c))) = ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c))))
11		ax-a2 31	. . . . . . . 8 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ (a →₁c)^⊥ ) = ((a →₁c)^⊥ ∪ (d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ )
12		oran3 93	. . . . . . . 8 ((a →₁c)^⊥ ∪ (d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥
13	11, 12	ax-r2 36	. . . . . . 7 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ (a →₁c)^⊥ ) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥
14	13	ax-r5 38	. . . . . 6 (((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ (a →₁c)^⊥ ) ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
15		df-i1 44	. . . . . . . . 9 ((a →₁c) →₁(b →₁c)) = ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
16	15	lor 70	. . . . . . . 8 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c) →₁(b →₁c))) = ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c))))
17	16	ax-r1 35	. . . . . . 7 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c)))) = ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c) →₁(b →₁c)))
18		oaidlem2.1	. . . . . . 7 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c) →₁(b →₁c))) = 1
19	17, 18	ax-r2 36	. . . . . 6 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c)))) = 1
20	10, 14, 19	3tr2 64	. . . . 5 (((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥ ∪ ((a →₁c) ∩ (b →₁c))) = 1
21	9, 20	lem3.1 443	. . . 4 ((a →₁c) ∩ (b →₁c)) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
22	21	ax-r1 35	. . 3 ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c)))) = ((a →₁c) ∩ (b →₁c))
23	22	bile 142	. 2 ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c)))) ≤ ((a →₁c) ∩ (b →₁c))
24		lear 161	. 2 ((a →₁c) ∩ (b →₁c)) ≤ (b →₁c)
25	23, 24	letr 137	1 ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)

Colors of variables: term

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

This theorem was proved from axioms: ax-a1 30 ax-a2 31 ax-a3 32 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

This theorem is referenced by: (None)

W3C validator