Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem negantlem2 831

Description: Lemma for negated antecedent identity.

**Hypothesis**
Ref	Expression
negant.1	(a →₁c) = (b →₁c)

**Assertion**
Ref	Expression
negantlem2	a ≤ (b^⊥ →₁c)

**Proof of Theorem negantlem2**
Step	Hyp	Ref	Expression
1		leo 150	. 2 a ≤ (a ∪ (b^⊥ →₁c))
2		i1orni1 829	. . . . . 6 ((b →₁c) ∪ (b^⊥ →₁c)) = 1
3	2	lan 70	. . . . 5 ((a ∪ (b^⊥ →₁c)) ∩ ((b →₁c) ∪ (b^⊥ →₁c))) = ((a ∪ (b^⊥ →₁c)) ∩ 1)
4	3	ax-r1 34	. . . 4 ((a ∪ (b^⊥ →₁c)) ∩ 1) = ((a ∪ (b^⊥ →₁c)) ∩ ((b →₁c) ∪ (b^⊥ →₁c)))
5		an1 98	. . . . 5 ((a ∪ (b^⊥ →₁c)) ∩ 1) = (a ∪ (b^⊥ →₁c))
6	5	ax-r1 34	. . . 4 (a ∪ (b^⊥ →₁c)) = ((a ∪ (b^⊥ →₁c)) ∩ 1)
7		u1lemc6 688	. . . . 5 (b →₁c) C (b^⊥ →₁c)
8		negant.1	. . . . . . 7 (a →₁c) = (b →₁c)
9	8	negantlem1 830	. . . . . 6 a C (b →₁c)
10	9	comcom 435	. . . . 5 (b →₁c) C a
11	7, 10	fh4rc 464	. . . 4 ((a ∩ (b →₁c)) ∪ (b^⊥ →₁c)) = ((a ∪ (b^⊥ →₁c)) ∩ ((b →₁c) ∪ (b^⊥ →₁c)))
12	4, 6, 11	3tr1 60	. . 3 (a ∪ (b^⊥ →₁c)) = ((a ∩ (b →₁c)) ∪ (b^⊥ →₁c))
13		ancom 68	. . . . . . . 8 (a ∩ (a →₁c)) = ((a →₁c) ∩ a)
14	8	lan 70	. . . . . . . 8 (a ∩ (a →₁c)) = (a ∩ (b →₁c))
15		u1lemaa 582	. . . . . . . 8 ((a →₁c) ∩ a) = (a ∩ c)
16	13, 14, 15	3tr2 61	. . . . . . 7 (a ∩ (b →₁c)) = (a ∩ c)
17		lear 153	. . . . . . 7 (a ∩ c) ≤ c
18	16, 17	bltr 130	. . . . . 6 (a ∩ (b →₁c)) ≤ c
19		lear 153	. . . . . 6 (a ∩ (b →₁c)) ≤ (b →₁c)
20	18, 19	ler2an 165	. . . . 5 (a ∩ (b →₁c)) ≤ (c ∩ (b →₁c))
21		lea 152	. . . . . . . 8 (b ∩ c) ≤ b
22		ax-a1 29	. . . . . . . 8 b = b^⊥ ^⊥
23	21, 22	lbtr 131	. . . . . . 7 (b ∩ c) ≤ b^⊥ ^⊥
24	23	leror 144	. . . . . 6 ((b ∩ c) ∪ (b^⊥ ∩ c)) ≤ (b^⊥ ^⊥ ∪ (b^⊥ ∩ c))
25		ancom 68	. . . . . . 7 (c ∩ (b →₁c)) = ((b →₁c) ∩ c)
26		u1lemab 592	. . . . . . 7 ((b →₁c) ∩ c) = ((b ∩ c) ∪ (b^⊥ ∩ c))
27	25, 26	ax-r2 35	. . . . . 6 (c ∩ (b →₁c)) = ((b ∩ c) ∪ (b^⊥ ∩ c))
28		df-i1 43	. . . . . 6 (b^⊥ →₁c) = (b^⊥ ^⊥ ∪ (b^⊥ ∩ c))
29	24, 27, 28	le3tr1 132	. . . . 5 (c ∩ (b →₁c)) ≤ (b^⊥ →₁c)
30	20, 29	letr 129	. . . 4 (a ∩ (b →₁c)) ≤ (b^⊥ →₁c)
31		leid 140	. . . 4 (b^⊥ →₁c) ≤ (b^⊥ →₁c)
32	30, 31	lel2or 162	. . 3 ((a ∩ (b →₁c)) ∪ (b^⊥ →₁c)) ≤ (b^⊥ →₁c)
33	12, 32	bltr 130	. 2 (a ∪ (b^⊥ →₁c)) ≤ (b^⊥ →₁c)
34	1, 33	letr 129	1 a ≤ (b^⊥ →₁c)

Colors of variables: term

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

This theorem is referenced by: negantlem4 833

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

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 df-c1 124 df-c2 125

metamath.org