QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  go2n6 GIF 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 gh
go2n6.2 hi
go2n6.3 ij
go2n6.4 jk
go2n6.5 km
go2n6.6 mn
go2n6.7 nu
go2n6.8 uw
go2n6.9 wx
go2n6.10 xy
go2n6.11 yz
go2n6.12 zg
go2n6.13 (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)
Assertion
Ref Expression
go2n6 (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) ≤ (hi)

Proof of Theorem go2n6
StepHypRef Expression
1 anass 76 . . . . . . . . . 10 (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) = ((wx) ∩ ((nu) ∩ ((km) ∩ (ij))))
2 ancom 74 . . . . . . . . . . . . 13 ((km) ∩ (ij)) = ((ij) ∩ (km))
32lan 77 . . . . . . . . . . . 12 ((nu) ∩ ((km) ∩ (ij))) = ((nu) ∩ ((ij) ∩ (km)))
4 ancom 74 . . . . . . . . . . . 12 ((nu) ∩ ((ij) ∩ (km))) = (((ij) ∩ (km)) ∩ (nu))
5 anass 76 . . . . . . . . . . . 12 (((ij) ∩ (km)) ∩ (nu)) = ((ij) ∩ ((km) ∩ (nu)))
63, 4, 53tr 65 . . . . . . . . . . 11 ((nu) ∩ ((km) ∩ (ij))) = ((ij) ∩ ((km) ∩ (nu)))
76lan 77 . . . . . . . . . 10 ((wx) ∩ ((nu) ∩ ((km) ∩ (ij)))) = ((wx) ∩ ((ij) ∩ ((km) ∩ (nu))))
8 ancom 74 . . . . . . . . . 10 ((wx) ∩ ((ij) ∩ ((km) ∩ (nu)))) = (((ij) ∩ ((km) ∩ (nu))) ∩ (wx))
91, 7, 83tr 65 . . . . . . . . 9 (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) = (((ij) ∩ ((km) ∩ (nu))) ∩ (wx))
109ran 78 . . . . . . . 8 ((((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) ∩ (yz)) = ((((ij) ∩ ((km) ∩ (nu))) ∩ (wx)) ∩ (yz))
11 anass 76 . . . . . . . 8 ((((ij) ∩ ((km) ∩ (nu))) ∩ (wx)) ∩ (yz)) = (((ij) ∩ ((km) ∩ (nu))) ∩ ((wx) ∩ (yz)))
1210, 11ax-r2 36 . . . . . . 7 ((((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) ∩ (yz)) = (((ij) ∩ ((km) ∩ (nu))) ∩ ((wx) ∩ (yz)))
1312ax-r1 35 . . . . . 6 (((ij) ∩ ((km) ∩ (nu))) ∩ ((wx) ∩ (yz))) = ((((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) ∩ (yz))
14 anass 76 . . . . . 6 (((ij) ∩ ((km) ∩ (nu))) ∩ ((wx) ∩ (yz))) = ((ij) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz))))
15 ancom 74 . . . . . 6 ((((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) ∩ (yz)) = ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))))
1613, 14, 153tr2 64 . . . . 5 ((ij) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) = ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))))
1716lan 77 . . . 4 ((gh) ∩ ((ij) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz))))) = ((gh) ∩ ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij)))))
18 anass 76 . . . 4 (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) = ((gh) ∩ ((ij) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))))
19 anass 76 . . . 4 (((gh) ∩ (yz)) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij)))) = ((gh) ∩ ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij)))))
2017, 18, 193tr1 63 . . 3 (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) = (((gh) ∩ (yz)) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))))
2120, 19ax-r2 36 . 2 (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) = ((gh) ∩ ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij)))))
22 go2n6.1 . . 3 gh
23 go2n6.2 . . 3 hi
24 anass 76 . . . . 5 (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) = ((i2 g) ∩ ((g2 y) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))))
2524ax-r1 35 . . . 4 ((i2 g) ∩ ((g2 y) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i))))) = (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i))))
26 go2n6.13 . . . 4 (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)
2725, 26bltr 138 . . 3 ((i2 g) ∩ ((g2 y) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i))))) ≤ (g2 i)
28 go2n6.11 . . . . 5 yz
29 go2n6.12 . . . . 5 zg
3028, 29govar2 897 . . . 4 (yz) ≤ (g2 y)
31 go2n6.9 . . . . . . 7 wx
32 go2n6.10 . . . . . . 7 xy
3331, 32govar2 897 . . . . . 6 (wx) ≤ (y2 w)
34 go2n6.7 . . . . . . 7 nu
35 go2n6.8 . . . . . . 7 uw
3634, 35govar2 897 . . . . . 6 (nu) ≤ (w2 n)
3733, 36le2an 169 . . . . 5 ((wx) ∩ (nu)) ≤ ((y2 w) ∩ (w2 n))
38 go2n6.5 . . . . . . 7 km
39 go2n6.6 . . . . . . 7 mn
4038, 39govar2 897 . . . . . 6 (km) ≤ (n2 k)
41 go2n6.3 . . . . . . 7 ij
42 go2n6.4 . . . . . . 7 jk
4341, 42govar2 897 . . . . . 6 (ij) ≤ (k2 i)
4440, 43le2an 169 . . . . 5 ((km) ∩ (ij)) ≤ ((n2 k) ∩ (k2 i))
4537, 44le2an 169 . . . 4 (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))) ≤ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))
4630, 45le2an 169 . . 3 ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij)))) ≤ ((g2 y) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i))))
4722, 23, 27, 46gon2n 898 . 2 ((gh) ∩ ((yz) ∩ (((wx) ∩ (nu)) ∩ ((km) ∩ (ij))))) ≤ (hi)
4821, 47bltr 138 1 (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) ≤ (hi)
Colors of variables: term
Syntax hints:  wle 2   wn 4  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