Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem negantlem10 843

Description: Lemma for negated antecedent identity.

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

**Assertion**
Ref	Expression
negantlem10	(a →₄c) ≤ (b →₄c)

**Proof of Theorem negantlem10**
Step	Hyp	Ref	Expression
1		leao4 157	. . . . 5 (a ∩ c) ≤ (b^⊥ ∪ c)
2		leor 151	. . . . . . . 8 (a ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
3		df-i1 43	. . . . . . . . 9 (a →₁c) = (a^⊥ ∪ (a ∩ c))
4	3	ax-r1 34	. . . . . . . 8 (a^⊥ ∪ (a ∩ c)) = (a →₁c)
5	2, 4	lbtr 131	. . . . . . 7 (a ∩ c) ≤ (a →₁c)
6		lear 153	. . . . . . 7 (a ∩ c) ≤ c
7	5, 6	ler2an 165	. . . . . 6 (a ∩ c) ≤ ((a →₁c) ∩ c)
8		negant.1	. . . . . . . 8 (a →₁c) = (b →₁c)
9	8	ran 71	. . . . . . 7 ((a →₁c) ∩ c) = ((b →₁c) ∩ c)
10		u1lemab 592	. . . . . . . 8 ((b →₁c) ∩ c) = ((b ∩ c) ∪ (b^⊥ ∩ c))
11		leor 151	. . . . . . . . 9 ((b ∩ c) ∪ (b^⊥ ∩ c)) ≤ (c^⊥ ∪ ((b ∩ c) ∪ (b^⊥ ∩ c)))
12		ancom 68	. . . . . . . . . . . . 13 (b ∩ c) = (c ∩ b)
13		ancom 68	. . . . . . . . . . . . 13 (b^⊥ ∩ c) = (c ∩ b^⊥ )
14	12, 13	2or 67	. . . . . . . . . . . 12 ((b ∩ c) ∪ (b^⊥ ∩ c)) = ((c ∩ b) ∪ (c ∩ b^⊥ ))
15		ax-a2 30	. . . . . . . . . . . 12 ((c ∩ b) ∪ (c ∩ b^⊥ )) = ((c ∩ b^⊥ ) ∪ (c ∩ b))
16	14, 15	ax-r2 35	. . . . . . . . . . 11 ((b ∩ c) ∪ (b^⊥ ∩ c)) = ((c ∩ b^⊥ ) ∪ (c ∩ b))
17	16	lor 66	. . . . . . . . . 10 (c^⊥ ∪ ((b ∩ c) ∪ (b^⊥ ∩ c))) = (c^⊥ ∪ ((c ∩ b^⊥ ) ∪ (c ∩ b)))
18		ax-a3 31	. . . . . . . . . . 11 ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)) = (c^⊥ ∪ ((c ∩ b^⊥ ) ∪ (c ∩ b)))
19	18	ax-r1 34	. . . . . . . . . 10 (c^⊥ ∪ ((c ∩ b^⊥ ) ∪ (c ∩ b))) = ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
20	17, 19	ax-r2 35	. . . . . . . . 9 (c^⊥ ∪ ((b ∩ c) ∪ (b^⊥ ∩ c))) = ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
21	11, 20	lbtr 131	. . . . . . . 8 ((b ∩ c) ∪ (b^⊥ ∩ c)) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
22	10, 21	bltr 130	. . . . . . 7 ((b →₁c) ∩ c) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
23	9, 22	bltr 130	. . . . . 6 ((a →₁c) ∩ c) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
24	7, 23	letr 129	. . . . 5 (a ∩ c) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
25	1, 24	ler2an 165	. . . 4 (a ∩ c) ≤ ((b^⊥ ∪ c) ∩ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)))
26		leao4 157	. . . . 5 (a^⊥ ∩ c) ≤ (b^⊥ ∪ c)
27		leor 151	. . . . . . . 8 (a^⊥ ∩ c) ≤ (a^⊥ ^⊥ ∪ (a^⊥ ∩ c))
28		df-i1 43	. . . . . . . . 9 (a^⊥ →₁c) = (a^⊥ ^⊥ ∪ (a^⊥ ∩ c))
29	28	ax-r1 34	. . . . . . . 8 (a^⊥ ^⊥ ∪ (a^⊥ ∩ c)) = (a^⊥ →₁c)
30	27, 29	lbtr 131	. . . . . . 7 (a^⊥ ∩ c) ≤ (a^⊥ →₁c)
31		lear 153	. . . . . . 7 (a^⊥ ∩ c) ≤ c
32	30, 31	ler2an 165	. . . . . 6 (a^⊥ ∩ c) ≤ ((a^⊥ →₁c) ∩ c)
33	8	negant 834	. . . . . . . 8 (a^⊥ →₁c) = (b^⊥ →₁c)
34	33	ran 71	. . . . . . 7 ((a^⊥ →₁c) ∩ c) = ((b^⊥ →₁c) ∩ c)
35		u1lemab 592	. . . . . . . 8 ((b^⊥ →₁c) ∩ c) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
36		leor 151	. . . . . . . . 9 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ≤ (c^⊥ ∪ ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)))
37		ancom 68	. . . . . . . . . . . . 13 (c ∩ b^⊥ ) = (b^⊥ ∩ c)
38		ancom 68	. . . . . . . . . . . . . 14 (c ∩ b) = (b ∩ c)
39		ax-a1 29	. . . . . . . . . . . . . . 15 b = b^⊥ ^⊥
40	39	ran 71	. . . . . . . . . . . . . 14 (b ∩ c) = (b^⊥ ^⊥ ∩ c)
41	38, 40	ax-r2 35	. . . . . . . . . . . . 13 (c ∩ b) = (b^⊥ ^⊥ ∩ c)
42	37, 41	2or 67	. . . . . . . . . . . 12 ((c ∩ b^⊥ ) ∪ (c ∩ b)) = ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))
43	42	lor 66	. . . . . . . . . . 11 (c^⊥ ∪ ((c ∩ b^⊥ ) ∪ (c ∩ b))) = (c^⊥ ∪ ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)))
44	43	ax-r1 34	. . . . . . . . . 10 (c^⊥ ∪ ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))) = (c^⊥ ∪ ((c ∩ b^⊥ ) ∪ (c ∩ b)))
45	44, 19	ax-r2 35	. . . . . . . . 9 (c^⊥ ∪ ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c))) = ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
46	36, 45	lbtr 131	. . . . . . . 8 ((b^⊥ ∩ c) ∪ (b^⊥ ^⊥ ∩ c)) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
47	35, 46	bltr 130	. . . . . . 7 ((b^⊥ →₁c) ∩ c) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
48	34, 47	bltr 130	. . . . . 6 ((a^⊥ →₁c) ∩ c) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
49	32, 48	letr 129	. . . . 5 (a^⊥ ∩ c) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
50	26, 49	ler2an 165	. . . 4 (a^⊥ ∩ c) ≤ ((b^⊥ ∪ c) ∩ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)))
51	25, 50	lel2or 162	. . 3 ((a ∩ c) ∪ (a^⊥ ∩ c)) ≤ ((b^⊥ ∪ c) ∩ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)))
52		lea 152	. . . . 5 ((a^⊥ ∪ c) ∩ c^⊥ ) ≤ (a^⊥ ∪ c)
53	8	negantlem8 838	. . . . 5 (a^⊥ ∪ c) = (b^⊥ ∪ c)
54	52, 53	lbtr 131	. . . 4 ((a^⊥ ∪ c) ∩ c^⊥ ) ≤ (b^⊥ ∪ c)
55		leao2 155	. . . . 5 ((a^⊥ ∪ c) ∩ c^⊥ ) ≤ (c^⊥ ∪ (c ∩ b^⊥ ))
56	55	ler 141	. . . 4 ((a^⊥ ∪ c) ∩ c^⊥ ) ≤ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b))
57	54, 56	ler2an 165	. . 3 ((a^⊥ ∪ c) ∩ c^⊥ ) ≤ ((b^⊥ ∪ c) ∩ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)))
58	51, 57	lel2or 162	. 2 (((a ∩ c) ∪ (a^⊥ ∩ c)) ∪ ((a^⊥ ∪ c) ∩ c^⊥ )) ≤ ((b^⊥ ∪ c) ∩ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)))
59		df-i4 46	. 2 (a →₄c) = (((a ∩ c) ∪ (a^⊥ ∩ c)) ∪ ((a^⊥ ∪ c) ∩ c^⊥ ))
60		dfi4b 482	. 2 (b →₄c) = ((b^⊥ ∪ c) ∩ ((c^⊥ ∪ (c ∩ b^⊥ )) ∪ (c ∩ b)))
61	58, 59, 60	le3tr1 132	1 (a →₄c) ≤ (b →₄c)

Colors of variables: term

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

This theorem is referenced by: negant4 844

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-i3 45 df-i4 46 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org