Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem oaidlem2 911

Description: Lemma for identity-like OA law.

**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 103	. . . . . . . . . 10 ((a →₁c) ∩ (a →₁c)) = (a →₁c)
2	1	ax-r1 34	. . . . . . . . 9 (a →₁c) = ((a →₁c) ∩ (a →₁c))
3	2	ran 71	. . . . . . . 8 ((a →₁c) ∩ (b →₁c)) = (((a →₁c) ∩ (a →₁c)) ∩ (b →₁c))
4		anass 69	. . . . . . . 8 (((a →₁c) ∩ (a →₁c)) ∩ (b →₁c)) = ((a →₁c) ∩ ((a →₁c) ∩ (b →₁c)))
5	3, 4	ax-r2 35	. . . . . . 7 ((a →₁c) ∩ (b →₁c)) = ((a →₁c) ∩ ((a →₁c) ∩ (b →₁c)))
6		leor 151	. . . . . . . 8 ((a →₁c) ∩ (b →₁c)) ≤ (d ∪ ((a →₁c) ∩ (b →₁c)))
7	6	lelan 159	. . . . . . 7 ((a →₁c) ∩ ((a →₁c) ∩ (b →₁c))) ≤ ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
8	5, 7	bltr 130	. . . . . 6 ((a →₁c) ∩ (b →₁c)) ≤ ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
9	8	df-le2 123	. . . . 5 (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
10		ax-a3 31	. . . . . 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 30	. . . . . . . 8 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ (a →₁c)^⊥ ) = ((a →₁c)^⊥ ∪ (d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ )
12		oran3 85	. . . . . . . 8 ((a →₁c)^⊥ ∪ (d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥
13	11, 12	ax-r2 35	. . . . . . 7 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ (a →₁c)^⊥ ) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥
14	13	ax-r5 37	. . . . . 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 43	. . . . . . . . 9 ((a →₁c) →₁(b →₁c)) = ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
16	15	lor 66	. . . . . . . 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 34	. . . . . . 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 35	. . . . . 6 ((d ∪ ((a →₁c) ∩ (b →₁c)))^⊥ ∪ ((a →₁c)^⊥ ∪ ((a →₁c) ∩ (b →₁c)))) = 1
20	10, 14, 19	3tr2 61	. . . . 5 (((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))^⊥ ∪ ((a →₁c) ∩ (b →₁c))) = 1
21	9, 20	lem3.1 425	. . . 4 ((a →₁c) ∩ (b →₁c)) = ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c))))
22	21	ax-r1 34	. . 3 ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c)))) = ((a →₁c) ∩ (b →₁c))
23	22	bile 134	. 2 ((a →₁c) ∩ (d ∪ ((a →₁c) ∩ (b →₁c)))) ≤ ((a →₁c) ∩ (b →₁c))
24		lear 153	. 2 ((a →₁c) ∩ (b →₁c)) ≤ (b →₁c)
25	23, 24	letr 129	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 9 →₁wi1 13

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

metamath.org