QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  mhlem Unicode version
Theorem mhlem 876
Description: Lemma 7.1 of Kalmbach, p. 91.
Hypothesis
Ref Expression
mhlem.1 (a v b) =< (c v d)'
Assertion
Ref Expression
mhlem ((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))
Proof of Theorem mhlem
StepHypRef Expression
1 comor1 461 . . . . . . 7 (a v b) C a
2 comor2 462 . . . . . . 7 (a v b) C b
31, 2com2an 484 . . . . . 6 (a v b) C (a ^ b)
4 mhlem.1 . . . . . . . 8 (a v b) =< (c v d)'
54lecom 180 . . . . . . 7 (a v b) C (c v d)'
65comcom7 460 . . . . . 6 (a v b) C (c v d)
73, 6fh1r 473 . . . . 5 (((a ^ b) v (c v d)) ^ (a v b)) = (((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b)))
8 comor1 461 . . . . . . 7 (c v d) C c
9 comor2 462 . . . . . . 7 (c v d) C d
108, 9com2an 484 . . . . . 6 (c v d) C (c ^ d)
11 leao1 162 . . . . . . . . . 10 (a ^ b) =< (a v b)
1211, 4letr 137 . . . . . . . . 9 (a ^ b) =< (c v d)'
1312lecom 180 . . . . . . . 8 (a ^ b) C (c v d)'
1413comcom7 460 . . . . . . 7 (a ^ b) C (c v d)
1514comcom 453 . . . . . 6 (c v d) C (a ^ b)
1610, 15fh2rc 480 . . . . 5 (((a ^ b) v (c v d)) ^ (c ^ d)) = (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (c ^ d)))
177, 162or 72 . . . 4 ((((a ^ b) v (c v d)) ^ (a v b)) v (((a ^ b) v (c v d)) ^ (c ^ d))) = ((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (c ^ d))))
1811lerr 150 . . . . . . . 8 (a ^ b) =< ((c ^ d) v (a v b))
1918lecom 180 . . . . . . 7 (a ^ b) C ((c ^ d) v (a v b))
2014, 19fh3 471 . . . . . 6 ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b)))) = (((a ^ b) v (c v d)) ^ ((a ^ b) v ((c ^ d) v (a v b))))
21 id 59 . . . . . . . 8 ((a v c) ^ (b v d)) = ((a v c) ^ (b v d))
224mhlemlem1 874 . . . . . . . . 9 (((a v b) v c) ^ (a v (c v d))) = (a v c)
234mhlemlem2 875 . . . . . . . . 9 (((a v b) v d) ^ (b v (c v d))) = (b v d)
2422, 232an 79 . . . . . . . 8 ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d)))) = ((a v c) ^ (b v d))
2521, 21, 243tr1 63 . . . . . . 7 ((a v c) ^ (b v d)) = ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d))))
26 an4 86 . . . . . . . 8 ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d)))) = ((((a v b) v c) ^ ((a v b) v d)) ^ ((a v (c v d)) ^ (b v (c v d))))
27 ancom 74 . . . . . . . 8 ((((a v b) v c) ^ ((a v b) v d)) ^ ((a v (c v d)) ^ (b v (c v d)))) = (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d)))
28 ax-a2 31 . . . . . . . . . . 11 ((a v b) v (c ^ d)) = ((c ^ d) v (a v b))
2911df-le2 131 . . . . . . . . . . . . 13 ((a ^ b) v (a v b)) = (a v b)
3029lor 70 . . . . . . . . . . . 12 ((c ^ d) v ((a ^ b) v (a v b))) = ((c ^ d) v (a v b))
3130ax-r1 35 . . . . . . . . . . 11 ((c ^ d) v (a v b)) = ((c ^ d) v ((a ^ b) v (a v b)))
32 or12 80 . . . . . . . . . . 11 ((c ^ d) v ((a ^ b) v (a v b))) = ((a ^ b) v ((c ^ d) v (a v b)))
3328, 31, 323tr 65 . . . . . . . . . 10 ((a v b) v (c ^ d)) = ((a ^ b) v ((c ^ d) v (a v b)))
3433lan 77 . . . . . . . . 9 (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d))) = (((a ^ b) v (c v d)) ^ ((a ^ b) v ((c ^ d) v (a v b))))
35 leo 158 . . . . . . . . . . . . . . . 16 a =< (a v b)
3635, 4letr 137 . . . . . . . . . . . . . . 15 a =< (c v d)'
3736lecom 180 . . . . . . . . . . . . . 14 a C (c v d)'
3837comcom7 460 . . . . . . . . . . . . 13 a C (c v d)
3938comcom 453 . . . . . . . . . . . 12 (c v d) C a
40 leor 159 . . . . . . . . . . . . . . . 16 b =< (a v b)
4140, 4letr 137 . . . . . . . . . . . . . . 15 b =< (c v d)'
4241lecom 180 . . . . . . . . . . . . . 14 b C (c v d)'
4342comcom7 460 . . . . . . . . . . . . 13 b C (c v d)
4443comcom 453 . . . . . . . . . . . 12 (c v d) C b
4539, 44fh3r 475 . . . . . . . . . . 11 ((a ^ b) v (c v d)) = ((a v (c v d)) ^ (b v (c v d)))
46 leo 158 . . . . . . . . . . . . . . . 16 c =< (c v d)
474lecon3 157 . . . . . . . . . . . . . . . 16 (c v d) =< (a v b)'
4846, 47letr 137 . . . . . . . . . . . . . . 15 c =< (a v b)'
4948lecom 180 . . . . . . . . . . . . . 14 c C (a v b)'
5049comcom7 460 . . . . . . . . . . . . 13 c C (a v b)
5150comcom 453 . . . . . . . . . . . 12 (a v b) C c
52 leor 159 . . . . . . . . . . . . . . . 16 d =< (c v d)
5352, 47letr 137 . . . . . . . . . . . . . . 15 d =< (a v b)'
5453lecom 180 . . . . . . . . . . . . . 14 d C (a v b)'
5554comcom7 460 . . . . . . . . . . . . 13 d C (a v b)
5655comcom 453 . . . . . . . . . . . 12 (a v b) C d
5751, 56fh3 471 . . . . . . . . . . 11 ((a v b) v (c ^ d)) = (((a v b) v c) ^ ((a v b) v d))
5845, 572an 79 . . . . . . . . . 10 (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d))) = (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d)))
5958ax-r1 35 . . . . . . . . 9 (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d))) = (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d)))
6034, 59, 203tr1 63 . . . . . . . 8 (((a v (c v d)) ^ (b v (c v d))) ^ (((a v b) v c) ^ ((a v b) v d))) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
6126, 27, 603tr 65 . . . . . . 7 ((((a v b) v c) ^ (a v (c v d))) ^ (((a v b) v d) ^ (b v (c v d)))) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
6225, 61ax-r2 36 . . . . . 6 ((a v c) ^ (b v d)) = ((a ^ b) v ((c v d) ^ ((c ^ d) v (a v b))))
6320, 62, 343tr1 63 . . . . 5 ((a v c) ^ (b v d)) = (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d)))
643, 6com2or 483 . . . . . 6 (a v b) C ((a ^ b) v (c v d))
65 leao1 162 . . . . . . . . . 10 (c ^ d) =< (c v d)
6665, 47letr 137 . . . . . . . . 9 (c ^ d) =< (a v b)'
6766lecom 180 . . . . . . . 8 (c ^ d) C (a v b)'
6867comcom7 460 . . . . . . 7 (c ^ d) C (a v b)
6968comcom 453 . . . . . 6 (a v b) C (c ^ d)
7064, 69fh2 470 . . . . 5 (((a ^ b) v (c v d)) ^ ((a v b) v (c ^ d))) = ((((a ^ b) v (c v d)) ^ (a v b)) v (((a ^ b) v (c v d)) ^ (c ^ d)))
7163, 70ax-r2 36 . . . 4 ((a v c) ^ (b v d)) = ((((a ^ b) v (c v d)) ^ (a v b)) v (((a ^ b) v (c v d)) ^ (c ^ d)))
72 ax-a3 32 . . . 4 (((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v ((a ^ b) ^ (c ^ d))) v ((c v d) ^ (c ^ d))) = ((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (c ^ d))))
7317, 71, 723tr1 63 . . 3 ((a v c) ^ (b v d)) = (((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v ((a ^ b) ^ (c ^ d))) v ((c v d) ^ (c ^ d)))
74 ax-a3 32 . . . 4 ((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v ((a ^ b) ^ (c ^ d))) = (((a ^ b) ^ (a v b)) v (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d))))
7574ax-r5 38 . . 3 (((((a ^ b) ^ (a v b)) v ((c v d) ^ (a v b))) v ((a ^ b) ^ (c ^ d))) v ((c v d) ^ (c ^ d))) = ((((a ^ b) ^ (a v b)) v (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d)))) v ((c v d) ^ (c ^ d)))
7673, 75ax-r2 36 . 2 ((a v c) ^ (b v d)) = ((((a ^ b) ^ (a v b)) v (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d)))) v ((c v d) ^ (c ^ d)))
7711, 65le2an 169 . . . . . . . . 9 ((a ^ b) ^ (c ^ d)) =< ((a v b) ^ (c v d))
78 ancom 74 . . . . . . . . 9 ((a v b) ^ (c v d)) = ((c v d) ^ (a v b))
7977, 78lbtr 139 . . . . . . . 8 ((a ^ b) ^ (c ^ d)) =< ((c v d) ^ (a v b))
8079df-le2 131 . . . . . . 7 (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (a v b))) = ((c v d) ^ (a v b))
81 ax-a2 31 . . . . . . 7 (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d))) = (((a ^ b) ^ (c ^ d)) v ((c v d) ^ (a v b)))
8280, 81, 783tr1 63 . . . . . 6 (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d))) = ((a v b) ^ (c v d))
834ortha 438 . . . . . 6 ((a v b) ^ (c v d)) = 0
8482, 83ax-r2 36 . . . . 5 (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d))) = 0
8584lor 70 . . . 4 (((a ^ b) ^ (a v b)) v (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d)))) = (((a ^ b) ^ (a v b)) v 0)
86 or0 102 . . . 4 (((a ^ b) ^ (a v b)) v 0) = ((a ^ b) ^ (a v b))
8711df2le2 136 . . . 4 ((a ^ b) ^ (a v b)) = (a ^ b)
8885, 86, 873tr 65 . . 3 (((a ^ b) ^ (a v b)) v (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d)))) = (a ^ b)
89 lear 161 . . . 4 ((c v d) ^ (c ^ d)) =< (c ^ d)
90 leid 148 . . . . 5 (c ^ d) =< (c ^ d)
9165, 90ler2an 173 . . . 4 (c ^ d) =< ((c v d) ^ (c ^ d))
9289, 91lebi 145 . . 3 ((c v d) ^ (c ^ d)) = (c ^ d)
9388, 922or 72 . 2 ((((a ^ b) ^ (a v b)) v (((c v d) ^ (a v b)) v ((a ^ b) ^ (c ^ d)))) v ((c v d) ^ (c ^ d))) = ((a ^ b) v (c ^ d))
9476, 93ax-r2 36 1 ((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7  0wf 9
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  mhlem2  878
  Copyright terms: Public domain W3C validator