QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wfh2 Unicode version
Theorem wfh2 424
Description: Weak structural analog of Foulis-Holland Theorem.
Hypotheses
Ref Expression
wfh.1 C (a, b) = 1
wfh.2 C (a, c) = 1
Assertion
Ref Expression
wfh2 ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1
Proof of Theorem wfh2
StepHypRef Expression
1 wledi 405 . . 3 (((b ^ a) v (b ^ c)) =<2 (b ^ (a v c))) = 1
2 oran 87 . . . . . . . . . . . 12 ((b ^ a) v (b ^ c)) = ((b ^ a)' ^ (b ^ c)')'
32bi1 118 . . . . . . . . . . 11 (((b ^ a) v (b ^ c)) == ((b ^ a)' ^ (b ^ c)')') = 1
4 df-a 40 . . . . . . . . . . . . . . 15 (b ^ a) = (b' v a')'
54bi1 118 . . . . . . . . . . . . . 14 ((b ^ a) == (b' v a')') = 1
65wcon2 208 . . . . . . . . . . . . 13 ((b ^ a)' == (b' v a')) = 1
76wran 369 . . . . . . . . . . . 12 (((b ^ a)' ^ (b ^ c)') == ((b' v a') ^ (b ^ c)')) = 1
87wr4 199 . . . . . . . . . . 11 (((b ^ a)' ^ (b ^ c)')' == ((b' v a') ^ (b ^ c)')') = 1
93, 8wr2 371 . . . . . . . . . 10 (((b ^ a) v (b ^ c)) == ((b' v a') ^ (b ^ c)')') = 1
109wcon2 208 . . . . . . . . 9 (((b ^ a) v (b ^ c))' == ((b' v a') ^ (b ^ c)')) = 1
1110wlan 370 . . . . . . . 8 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)'))) = 1
12 an4 86 . . . . . . . . . 10 ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) = ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)'))
1312bi1 118 . . . . . . . . 9 (((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) == ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)'))) = 1
14 wfh.1 . . . . . . . . . . . . . 14 C (a, b) = 1
1514wcomcom 414 . . . . . . . . . . . . 13 C (b, a) = 1
1615wcomcom2 415 . . . . . . . . . . . 12 C (b, a') = 1
1716wcom3ii 419 . . . . . . . . . . 11 ((b ^ (b' v a')) == (b ^ a')) = 1
18 ancom 74 . . . . . . . . . . . 12 (b ^ a') = (a' ^ b)
1918bi1 118 . . . . . . . . . . 11 ((b ^ a') == (a' ^ b)) = 1
2017, 19wr2 371 . . . . . . . . . 10 ((b ^ (b' v a')) == (a' ^ b)) = 1
2120wran 369 . . . . . . . . 9 (((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)')) == ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))) = 1
2213, 21wr2 371 . . . . . . . 8 (((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) == ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))) = 1
2311, 22wr2 371 . . . . . . 7 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))) = 1
24 an4 86 . . . . . . . 8 ((a' ^ b) ^ ((a v c) ^ (b ^ c)')) = ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))
2524bi1 118 . . . . . . 7 (((a' ^ b) ^ ((a v c) ^ (b ^ c)')) == ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))) = 1
2623, 25wr2 371 . . . . . 6 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))) = 1
27 ax-a1 30 . . . . . . . . . . 11 a = a''
2827bi1 118 . . . . . . . . . 10 (a == a'') = 1
2928wr5-2v 366 . . . . . . . . 9 ((a v c) == (a'' v c)) = 1
3029wlan 370 . . . . . . . 8 ((a' ^ (a v c)) == (a' ^ (a'' v c))) = 1
31 wfh.2 . . . . . . . . . 10 C (a, c) = 1
3231wcomcom3 416 . . . . . . . . 9 C (a', c) = 1
3332wcom3ii 419 . . . . . . . 8 ((a' ^ (a'' v c)) == (a' ^ c)) = 1
3430, 33wr2 371 . . . . . . 7 ((a' ^ (a v c)) == (a' ^ c)) = 1
3534wran 369 . . . . . 6 (((a' ^ (a v c)) ^ (b ^ (b ^ c)')) == ((a' ^ c) ^ (b ^ (b ^ c)'))) = 1
3626, 35wr2 371 . . . . 5 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((a' ^ c) ^ (b ^ (b ^ c)'))) = 1
37 anass 76 . . . . . 6 ((a' ^ c) ^ (b ^ (b ^ c)')) = (a' ^ (c ^ (b ^ (b ^ c)')))
3837bi1 118 . . . . 5 (((a' ^ c) ^ (b ^ (b ^ c)')) == (a' ^ (c ^ (b ^ (b ^ c)')))) = 1
3936, 38wr2 371 . . . 4 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == (a' ^ (c ^ (b ^ (b ^ c)')))) = 1
40 anass 76 . . . . . . . . 9 ((b ^ c) ^ (b ^ c)') = (b ^ (c ^ (b ^ c)'))
4140bi1 118 . . . . . . . 8 (((b ^ c) ^ (b ^ c)') == (b ^ (c ^ (b ^ c)'))) = 1
4241wr1 197 . . . . . . 7 ((b ^ (c ^ (b ^ c)')) == ((b ^ c) ^ (b ^ c)')) = 1
43 an12 81 . . . . . . . 8 (c ^ (b ^ (b ^ c)')) = (b ^ (c ^ (b ^ c)'))
4443bi1 118 . . . . . . 7 ((c ^ (b ^ (b ^ c)')) == (b ^ (c ^ (b ^ c)'))) = 1
45 dff 101 . . . . . . . 8 0 = ((b ^ c) ^ (b ^ c)')
4645bi1 118 . . . . . . 7 (0 == ((b ^ c) ^ (b ^ c)')) = 1
4742, 44, 46w3tr1 374 . . . . . 6 ((c ^ (b ^ (b ^ c)')) == 0) = 1
4847wlan 370 . . . . 5 ((a' ^ (c ^ (b ^ (b ^ c)'))) == (a' ^ 0)) = 1
49 an0 108 . . . . . 6 (a' ^ 0) = 0
5049bi1 118 . . . . 5 ((a' ^ 0) == 0) = 1
5148, 50wr2 371 . . . 4 ((a' ^ (c ^ (b ^ (b ^ c)'))) == 0) = 1
5239, 51wr2 371 . . 3 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == 0) = 1
531, 52wom5 381 . 2 (((b ^ a) v (b ^ c)) == (b ^ (a v c))) = 1
5453wr1 197 1 ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8  0wf 9   C wcmtr 29
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-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134
This theorem is referenced by:  wfh4  426
  Copyright terms: Public domain W3C validator