QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  go2n6 Unicode version
Theorem go2n6 901
Description: 12-variable Godowski equation derived from 6-variable one. The last hypothesis is the 6-variable Godowski equation.
Hypotheses
Ref Expression
go2n6.1 g =< h'
go2n6.2 h =< i'
go2n6.3 i =< j'
go2n6.4 j =< k'
go2n6.5 k =< m'
go2n6.6 m =< n'
go2n6.7 n =< u'
go2n6.8 u =< w'
go2n6.9 w =< x'
go2n6.10 x =< y'
go2n6.11 y =< z'
go2n6.12 z =< g'
go2n6.13 (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) =< (g ->2 i)
Assertion
Ref Expression
go2n6 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) =< (h v i)
Proof of Theorem go2n6
StepHypRef Expression
1 anass 76 . . . . . . . . . 10 (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) = ((w v x) ^ ((n v u) ^ ((k v m) ^ (i v j))))
2 ancom 74 . . . . . . . . . . . . 13 ((k v m) ^ (i v j)) = ((i v j) ^ (k v m))
32lan 77 . . . . . . . . . . . 12 ((n v u) ^ ((k v m) ^ (i v j))) = ((n v u) ^ ((i v j) ^ (k v m)))
4 ancom 74 . . . . . . . . . . . 12 ((n v u) ^ ((i v j) ^ (k v m))) = (((i v j) ^ (k v m)) ^ (n v u))
5 anass 76 . . . . . . . . . . . 12 (((i v j) ^ (k v m)) ^ (n v u)) = ((i v j) ^ ((k v m) ^ (n v u)))
63, 4, 53tr 65 . . . . . . . . . . 11 ((n v u) ^ ((k v m) ^ (i v j))) = ((i v j) ^ ((k v m) ^ (n v u)))
76lan 77 . . . . . . . . . 10 ((w v x) ^ ((n v u) ^ ((k v m) ^ (i v j)))) = ((w v x) ^ ((i v j) ^ ((k v m) ^ (n v u))))
8 ancom 74 . . . . . . . . . 10 ((w v x) ^ ((i v j) ^ ((k v m) ^ (n v u)))) = (((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x))
91, 7, 83tr 65 . . . . . . . . 9 (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) = (((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x))
109ran 78 . . . . . . . 8 ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z)) = ((((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x)) ^ (y v z))
11 anass 76 . . . . . . . 8 ((((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x)) ^ (y v z)) = (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z)))
1210, 11ax-r2 36 . . . . . . 7 ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z)) = (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z)))
1312ax-r1 35 . . . . . 6 (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z))) = ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z))
14 anass 76 . . . . . 6 (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z))) = ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z))))
15 ancom 74 . . . . . 6 ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z)) = ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))
1613, 14, 153tr2 64 . . . . 5 ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))
1716lan 77 . . . 4 ((g v h) ^ ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z))))) = ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))))
18 anass 76 . . . 4 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = ((g v h) ^ ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))))
19 anass 76 . . . 4 (((g v h) ^ (y v z)) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))) = ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))))
2017, 18, 193tr1 63 . . 3 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = (((g v h) ^ (y v z)) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))
2120, 19ax-r2 36 . 2 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))))
22 go2n6.1 . . 3 g =< h'
23 go2n6.2 . . 3 h =< i'
24 anass 76 . . . . 5 (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) = ((i ->2 g) ^ ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))))
2524ax-r1 35 . . . 4 ((i ->2 g) ^ ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))) = (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))
26 go2n6.13 . . . 4 (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) =< (g ->2 i)
2725, 26bltr 138 . . 3 ((i ->2 g) ^ ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))) =< (g ->2 i)
28 go2n6.11 . . . . 5 y =< z'
29 go2n6.12 . . . . 5 z =< g'
3028, 29govar2 897 . . . 4 (y v z) =< (g ->2 y)
31 go2n6.9 . . . . . . 7 w =< x'
32 go2n6.10 . . . . . . 7 x =< y'
3331, 32govar2 897 . . . . . 6 (w v x) =< (y ->2 w)
34 go2n6.7 . . . . . . 7 n =< u'
35 go2n6.8 . . . . . . 7 u =< w'
3634, 35govar2 897 . . . . . 6 (n v u) =< (w ->2 n)
3733, 36le2an 169 . . . . 5 ((w v x) ^ (n v u)) =< ((y ->2 w) ^ (w ->2 n))
38 go2n6.5 . . . . . . 7 k =< m'
39 go2n6.6 . . . . . . 7 m =< n'
4038, 39govar2 897 . . . . . 6 (k v m) =< (n ->2 k)
41 go2n6.3 . . . . . . 7 i =< j'
42 go2n6.4 . . . . . . 7 j =< k'
4341, 42govar2 897 . . . . . 6 (i v j) =< (k ->2 i)
4440, 43le2an 169 . . . . 5 ((k v m) ^ (i v j)) =< ((n ->2 k) ^ (k ->2 i))
4537, 44le2an 169 . . . 4 (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) =< (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))
4630, 45le2an 169 . . 3 ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))) =< ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))
4722, 23, 27, 46gon2n 898 . 2 ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))) =< (h v i)
4821, 47bltr 138 1 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) =< (h v i)
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7   ->2 wi2 13
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-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  gomaex3lem5  918
  Copyright terms: Public domain W3C validator