QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa8to5 Unicode version
Theorem oa8to5 972
Description: Orthoarguesian law 5OA converted from 8 to 5 variables.
Hypotheses
Ref Expression
oa8to5.1 (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h'))) =< (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))
oa8to5.2 b' = (a ->1 j)'
oa8to5.3 d' = (c ->1 j)'
oa8to5.4 f' = (e ->1 j)'
oa8to5.5 h' = (g ->1 j)'
Assertion
Ref Expression
oa8to5 ((a ->1 j) ^ (a v (c ^ ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))))))) =< (((a ^ j) v (c ^ j)) v ((e ^ j) v (g ^ j)))
Proof of Theorem oa8to5
StepHypRef Expression
1 oa8to5.1 . . 3 (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h'))) =< (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))
21oa8todual 971 . 2 (b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) =< (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h)))
3 oa8to5.2 . . . 4 b' = (a ->1 j)'
43con1 66 . . 3 b = (a ->1 j)
5 oa8to5.3 . . . . . . . . . 10 d' = (c ->1 j)'
65con1 66 . . . . . . . . 9 d = (c ->1 j)
74, 62an 79 . . . . . . . 8 (b ^ d) = ((a ->1 j) ^ (c ->1 j))
87lor 70 . . . . . . 7 ((a ^ c) v (b ^ d)) = ((a ^ c) v ((a ->1 j) ^ (c ->1 j)))
9 oa8to5.5 . . . . . . . . . . 11 h' = (g ->1 j)'
109con1 66 . . . . . . . . . 10 h = (g ->1 j)
114, 102an 79 . . . . . . . . 9 (b ^ h) = ((a ->1 j) ^ (g ->1 j))
1211lor 70 . . . . . . . 8 ((a ^ g) v (b ^ h)) = ((a ^ g) v ((a ->1 j) ^ (g ->1 j)))
136, 102an 79 . . . . . . . . 9 (d ^ h) = ((c ->1 j) ^ (g ->1 j))
1413lor 70 . . . . . . . 8 ((c ^ g) v (d ^ h)) = ((c ^ g) v ((c ->1 j) ^ (g ->1 j)))
1512, 142an 79 . . . . . . 7 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))
168, 152or 72 . . . . . 6 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j)))))
17 oa8to5.4 . . . . . . . . . . 11 f' = (e ->1 j)'
1817con1 66 . . . . . . . . . 10 f = (e ->1 j)
194, 182an 79 . . . . . . . . 9 (b ^ f) = ((a ->1 j) ^ (e ->1 j))
2019lor 70 . . . . . . . 8 ((a ^ e) v (b ^ f)) = ((a ^ e) v ((a ->1 j) ^ (e ->1 j)))
2118, 102an 79 . . . . . . . . . 10 (f ^ h) = ((e ->1 j) ^ (g ->1 j))
2221lor 70 . . . . . . . . 9 ((e ^ g) v (f ^ h)) = ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))
2312, 222an 79 . . . . . . . 8 (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h))) = (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))
2420, 232or 72 . . . . . . 7 (((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))
256, 182an 79 . . . . . . . . 9 (d ^ f) = ((c ->1 j) ^ (e ->1 j))
2625lor 70 . . . . . . . 8 ((c ^ e) v (d ^ f)) = ((c ^ e) v ((c ->1 j) ^ (e ->1 j)))
2714, 222an 79 . . . . . . . 8 (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))) = (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))
2826, 272or 72 . . . . . . 7 (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))
2924, 282an 79 . . . . . 6 ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))) = ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))))
3016, 292or 72 . . . . 5 ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))))) = ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))))
3130lan 77 . . . 4 (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))) = (c ^ ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))))))
3231lor 70 . . 3 (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))))))) = (a v (c ^ ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))))))
334, 322an 79 . 2 (b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) = ((a ->1 j) ^ (a v (c ^ ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))))))))
344lan 77 . . . . 5 (a ^ b) = (a ^ (a ->1 j))
35 ancom 74 . . . . 5 (a ^ (a ->1 j)) = ((a ->1 j) ^ a)
36 u1lemaa 600 . . . . 5 ((a ->1 j) ^ a) = (a ^ j)
3734, 35, 363tr 65 . . . 4 (a ^ b) = (a ^ j)
386lan 77 . . . . 5 (c ^ d) = (c ^ (c ->1 j))
39 ancom 74 . . . . 5 (c ^ (c ->1 j)) = ((c ->1 j) ^ c)
40 u1lemaa 600 . . . . 5 ((c ->1 j) ^ c) = (c ^ j)
4138, 39, 403tr 65 . . . 4 (c ^ d) = (c ^ j)
4237, 412or 72 . . 3 ((a ^ b) v (c ^ d)) = ((a ^ j) v (c ^ j))
4318lan 77 . . . . 5 (e ^ f) = (e ^ (e ->1 j))
44 ancom 74 . . . . 5 (e ^ (e ->1 j)) = ((e ->1 j) ^ e)
45 u1lemaa 600 . . . . 5 ((e ->1 j) ^ e) = (e ^ j)
4643, 44, 453tr 65 . . . 4 (e ^ f) = (e ^ j)
4710lan 77 . . . . 5 (g ^ h) = (g ^ (g ->1 j))
48 ancom 74 . . . . 5 (g ^ (g ->1 j)) = ((g ->1 j) ^ g)
49 u1lemaa 600 . . . . 5 ((g ->1 j) ^ g) = (g ^ j)
5047, 48, 493tr 65 . . . 4 (g ^ h) = (g ^ j)
5146, 502or 72 . . 3 ((e ^ f) v (g ^ h)) = ((e ^ j) v (g ^ j))
5242, 512or 72 . 2 (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h))) = (((a ^ j) v (c ^ j)) v ((e ^ j) v (g ^ j)))
532, 33, 52le3tr2 141 1 ((a ->1 j) ^ (a v (c ^ ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))))))) =< (((a ^ j) v (c ^ j)) v ((e ^ j) v (g ^ j)))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7   ->1 wi1 12
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator