Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3to4lem6 GIF version

Theorem oa3to4lem6 950
 Description: Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only.
Hypotheses
Ref Expression
oa3to4lem6.oa4.1 ab
oa3to4lem6.oa4.2 cd
oa3to4lem6.3 g = ((ab ) ∪ (cd ))
oa3to4lem6.4 e = a
oa3to4lem6.5 f = c
oa3to4lem6.oa3 (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))
Assertion
Ref Expression
oa3to4lem6 ((ab) ∩ (cd)) ≤ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))

Proof of Theorem oa3to4lem6
StepHypRef Expression
1 oa3to4lem6.oa4.1 . . . . . 6 ab
21lecon3 157 . . . . 5 ba
32lecon 154 . . . 4 a b
4 oa3to4lem6.oa4.2 . . . . . 6 cd
54lecon3 157 . . . . 5 dc
65lecon 154 . . . 4 c d
7 id 59 . . . 4 ((ab ) ∪ (cd )) = ((ab ) ∪ (cd ))
8 oa3to4lem6.oa3 . . . . 5 (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))
9 oa3to4lem6.4 . . . . . 6 e = a
10 oa3to4lem6.3 . . . . . . . 8 g = ((ab ) ∪ (cd ))
119, 10ud1lem0ab 257 . . . . . . 7 (e1 g) = (a1 ((ab ) ∪ (cd )))
12 oa3to4lem6.5 . . . . . . . . 9 f = c
1312, 10ud1lem0ab 257 . . . . . . . 8 (f1 g) = (c1 ((ab ) ∪ (cd )))
149, 122an 79 . . . . . . . . 9 (ef) = (ac )
1511, 132an 79 . . . . . . . . 9 ((e1 g) ∩ (f1 g)) = ((a1 ((ab ) ∪ (cd ))) ∩ (c1 ((ab ) ∪ (cd ))))
1614, 152or 72 . . . . . . . 8 ((ef) ∪ ((e1 g) ∩ (f1 g))) = ((ac ) ∪ ((a1 ((ab ) ∪ (cd ))) ∩ (c1 ((ab ) ∪ (cd )))))
1713, 162an 79 . . . . . . 7 ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))) = ((c1 ((ab ) ∪ (cd ))) ∩ ((ac ) ∪ ((a1 ((ab ) ∪ (cd ))) ∩ (c1 ((ab ) ∪ (cd ))))))
1811, 172or 72 . . . . . 6 ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g))))) = ((a1 ((ab ) ∪ (cd ))) ∪ ((c1 ((ab ) ∪ (cd ))) ∩ ((ac ) ∪ ((a1 ((ab ) ∪ (cd ))) ∩ (c1 ((ab ) ∪ (cd )))))))
199, 182an 79 . . . . 5 (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) = (a ∩ ((a1 ((ab ) ∪ (cd ))) ∪ ((c1 ((ab ) ∪ (cd ))) ∩ ((ac ) ∪ ((a1 ((ab ) ∪ (cd ))) ∩ (c1 ((ab ) ∪ (cd ))))))))
209, 102an 79 . . . . . 6 (eg) = (a ∩ ((ab ) ∪ (cd )))
2112, 102an 79 . . . . . 6 (fg) = (c ∩ ((ab ) ∪ (cd )))
2220, 212or 72 . . . . 5 ((eg) ∪ (fg)) = ((a ∩ ((ab ) ∪ (cd ))) ∪ (c ∩ ((ab ) ∪ (cd ))))
238, 19, 22le3tr2 141 . . . 4 (a ∩ ((a1 ((ab ) ∪ (cd ))) ∪ ((c1 ((ab ) ∪ (cd ))) ∩ ((ac ) ∪ ((a1 ((ab ) ∪ (cd ))) ∩ (c1 ((ab ) ∪ (cd )))))))) ≤ ((a ∩ ((ab ) ∪ (cd ))) ∪ (c ∩ ((ab ) ∪ (cd ))))
243, 6, 7, 23oa3to4lem4 948 . . 3 (a ∩ (b ∪ (d ∩ ((ac ) ∪ (bd ))))) ≤ ((ab ) ∪ (cd ))
25 anor3 90 . . . . . . . . . . 11 (ac ) = (ac)
26 anor3 90 . . . . . . . . . . 11 (bd ) = (bd)
2725, 262or 72 . . . . . . . . . 10 ((ac ) ∪ (bd )) = ((ac) ∪ (bd) )
28 oran3 93 . . . . . . . . . 10 ((ac) ∪ (bd) ) = ((ac) ∩ (bd))
2927, 28ax-r2 36 . . . . . . . . 9 ((ac ) ∪ (bd )) = ((ac) ∩ (bd))
3029lan 77 . . . . . . . 8 (d ∩ ((ac ) ∪ (bd ))) = (d ∩ ((ac) ∩ (bd)) )
31 anor3 90 . . . . . . . 8 (d ∩ ((ac) ∩ (bd)) ) = (d ∪ ((ac) ∩ (bd)))
3230, 31ax-r2 36 . . . . . . 7 (d ∩ ((ac ) ∪ (bd ))) = (d ∪ ((ac) ∩ (bd)))
3332lor 70 . . . . . 6 (b ∪ (d ∩ ((ac ) ∪ (bd )))) = (b ∪ (d ∪ ((ac) ∩ (bd))) )
34 oran3 93 . . . . . 6 (b ∪ (d ∪ ((ac) ∩ (bd))) ) = (b ∩ (d ∪ ((ac) ∩ (bd))))
3533, 34ax-r2 36 . . . . 5 (b ∪ (d ∩ ((ac ) ∪ (bd )))) = (b ∩ (d ∪ ((ac) ∩ (bd))))
3635lan 77 . . . 4 (a ∩ (b ∪ (d ∩ ((ac ) ∪ (bd ))))) = (a ∩ (b ∩ (d ∪ ((ac) ∩ (bd)))) )
37 anor3 90 . . . 4 (a ∩ (b ∩ (d ∪ ((ac) ∩ (bd)))) ) = (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))
3836, 37ax-r2 36 . . 3 (a ∩ (b ∪ (d ∩ ((ac ) ∪ (bd ))))) = (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))
39 anor3 90 . . . . 5 (ab ) = (ab)
40 anor3 90 . . . . 5 (cd ) = (cd)
4139, 402or 72 . . . 4 ((ab ) ∪ (cd )) = ((ab) ∪ (cd) )
42 oran3 93 . . . 4 ((ab) ∪ (cd) ) = ((ab) ∩ (cd))
4341, 42ax-r2 36 . . 3 ((ab ) ∪ (cd )) = ((ab) ∩ (cd))
4424, 38, 43le3tr2 141 . 2 (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd))))) ≤ ((ab) ∩ (cd))
4544lecon1 155 1 ((ab) ∩ (cd)) ≤ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2  ⊥ wn 4   ∪ 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:  oa3to4  951
 Copyright terms: Public domain W3C validator