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

Theorem negantlem10 861
Description: Lemma for negated antecedent identity.
Hypothesis
Ref Expression
negant.1 (a1 c) = (b1 c)
Assertion
Ref Expression
negantlem10 (a4 c) ≤ (b4 c)

Proof of Theorem negantlem10
StepHypRef Expression
1 leao4 165 . . . . 5 (ac) ≤ (bc)
2 leor 159 . . . . . . . 8 (ac) ≤ (a ∪ (ac))
3 df-i1 44 . . . . . . . . 9 (a1 c) = (a ∪ (ac))
43ax-r1 35 . . . . . . . 8 (a ∪ (ac)) = (a1 c)
52, 4lbtr 139 . . . . . . 7 (ac) ≤ (a1 c)
6 lear 161 . . . . . . 7 (ac) ≤ c
75, 6ler2an 173 . . . . . 6 (ac) ≤ ((a1 c) ∩ c)
8 negant.1 . . . . . . . 8 (a1 c) = (b1 c)
98ran 78 . . . . . . 7 ((a1 c) ∩ c) = ((b1 c) ∩ c)
10 u1lemab 610 . . . . . . . 8 ((b1 c) ∩ c) = ((bc) ∪ (bc))
11 leor 159 . . . . . . . . 9 ((bc) ∪ (bc)) ≤ (c ∪ ((bc) ∪ (bc)))
12 ancom 74 . . . . . . . . . . . . 13 (bc) = (cb)
13 ancom 74 . . . . . . . . . . . . 13 (bc) = (cb )
1412, 132or 72 . . . . . . . . . . . 12 ((bc) ∪ (bc)) = ((cb) ∪ (cb ))
15 ax-a2 31 . . . . . . . . . . . 12 ((cb) ∪ (cb )) = ((cb ) ∪ (cb))
1614, 15ax-r2 36 . . . . . . . . . . 11 ((bc) ∪ (bc)) = ((cb ) ∪ (cb))
1716lor 70 . . . . . . . . . 10 (c ∪ ((bc) ∪ (bc))) = (c ∪ ((cb ) ∪ (cb)))
18 ax-a3 32 . . . . . . . . . . 11 ((c ∪ (cb )) ∪ (cb)) = (c ∪ ((cb ) ∪ (cb)))
1918ax-r1 35 . . . . . . . . . 10 (c ∪ ((cb ) ∪ (cb))) = ((c ∪ (cb )) ∪ (cb))
2017, 19ax-r2 36 . . . . . . . . 9 (c ∪ ((bc) ∪ (bc))) = ((c ∪ (cb )) ∪ (cb))
2111, 20lbtr 139 . . . . . . . 8 ((bc) ∪ (bc)) ≤ ((c ∪ (cb )) ∪ (cb))
2210, 21bltr 138 . . . . . . 7 ((b1 c) ∩ c) ≤ ((c ∪ (cb )) ∪ (cb))
239, 22bltr 138 . . . . . 6 ((a1 c) ∩ c) ≤ ((c ∪ (cb )) ∪ (cb))
247, 23letr 137 . . . . 5 (ac) ≤ ((c ∪ (cb )) ∪ (cb))
251, 24ler2an 173 . . . 4 (ac) ≤ ((bc) ∩ ((c ∪ (cb )) ∪ (cb)))
26 leao4 165 . . . . 5 (ac) ≤ (bc)
27 leor 159 . . . . . . . 8 (ac) ≤ (a ∪ (ac))
28 df-i1 44 . . . . . . . . 9 (a1 c) = (a ∪ (ac))
2928ax-r1 35 . . . . . . . 8 (a ∪ (ac)) = (a1 c)
3027, 29lbtr 139 . . . . . . 7 (ac) ≤ (a1 c)
31 lear 161 . . . . . . 7 (ac) ≤ c
3230, 31ler2an 173 . . . . . 6 (ac) ≤ ((a1 c) ∩ c)
338negant 852 . . . . . . . 8 (a1 c) = (b1 c)
3433ran 78 . . . . . . 7 ((a1 c) ∩ c) = ((b1 c) ∩ c)
35 u1lemab 610 . . . . . . . 8 ((b1 c) ∩ c) = ((bc) ∪ (b c))
36 leor 159 . . . . . . . . 9 ((bc) ∪ (b c)) ≤ (c ∪ ((bc) ∪ (b c)))
37 ancom 74 . . . . . . . . . . . . 13 (cb ) = (bc)
38 ancom 74 . . . . . . . . . . . . . 14 (cb) = (bc)
39 ax-a1 30 . . . . . . . . . . . . . . 15 b = b
4039ran 78 . . . . . . . . . . . . . 14 (bc) = (b c)
4138, 40ax-r2 36 . . . . . . . . . . . . 13 (cb) = (b c)
4237, 412or 72 . . . . . . . . . . . 12 ((cb ) ∪ (cb)) = ((bc) ∪ (b c))
4342lor 70 . . . . . . . . . . 11 (c ∪ ((cb ) ∪ (cb))) = (c ∪ ((bc) ∪ (b c)))
4443ax-r1 35 . . . . . . . . . 10 (c ∪ ((bc) ∪ (b c))) = (c ∪ ((cb ) ∪ (cb)))
4544, 19ax-r2 36 . . . . . . . . 9 (c ∪ ((bc) ∪ (b c))) = ((c ∪ (cb )) ∪ (cb))
4636, 45lbtr 139 . . . . . . . 8 ((bc) ∪ (b c)) ≤ ((c ∪ (cb )) ∪ (cb))
4735, 46bltr 138 . . . . . . 7 ((b1 c) ∩ c) ≤ ((c ∪ (cb )) ∪ (cb))
4834, 47bltr 138 . . . . . 6 ((a1 c) ∩ c) ≤ ((c ∪ (cb )) ∪ (cb))
4932, 48letr 137 . . . . 5 (ac) ≤ ((c ∪ (cb )) ∪ (cb))
5026, 49ler2an 173 . . . 4 (ac) ≤ ((bc) ∩ ((c ∪ (cb )) ∪ (cb)))
5125, 50lel2or 170 . . 3 ((ac) ∪ (ac)) ≤ ((bc) ∩ ((c ∪ (cb )) ∪ (cb)))
52 lea 160 . . . . 5 ((ac) ∩ c ) ≤ (ac)
538negantlem8 856 . . . . 5 (ac) = (bc)
5452, 53lbtr 139 . . . 4 ((ac) ∩ c ) ≤ (bc)
55 leao2 163 . . . . 5 ((ac) ∩ c ) ≤ (c ∪ (cb ))
5655ler 149 . . . 4 ((ac) ∩ c ) ≤ ((c ∪ (cb )) ∪ (cb))
5754, 56ler2an 173 . . 3 ((ac) ∩ c ) ≤ ((bc) ∩ ((c ∪ (cb )) ∪ (cb)))
5851, 57lel2or 170 . 2 (((ac) ∪ (ac)) ∪ ((ac) ∩ c )) ≤ ((bc) ∩ ((c ∪ (cb )) ∪ (cb)))
59 df-i4 47 . 2 (a4 c) = (((ac) ∪ (ac)) ∪ ((ac) ∩ c ))
60 dfi4b 500 . 2 (b4 c) = ((bc) ∩ ((c ∪ (cb )) ∪ (cb)))
6158, 59, 60le3tr1 140 1 (a4 c) ≤ (b4 c)
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  wo 6  wa 7  1 wi1 12  4 wi4 15
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  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-i3 46  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  negant4  862
  Copyright terms: Public domain W3C validator