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

Theorem oa3to4 951
 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
oa3to4.oa4.1 ab
oa3to4.oa4.2 cd
oa3to4.3 g = ((ba ) ∪ (dc ))
oa3to4.4 e = b
oa3to4.5 f = d
oa3to4.oa3 (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))
Assertion
Ref Expression
oa3to4 ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Proof of Theorem oa3to4
StepHypRef Expression
1 oa3to4.oa4.1 . . . 4 ab
21lecon3 157 . . 3 ba
3 oa3to4.oa4.2 . . . 4 cd
43lecon3 157 . . 3 dc
5 oa3to4.3 . . 3 g = ((ba ) ∪ (dc ))
6 oa3to4.4 . . 3 e = b
7 oa3to4.5 . . 3 f = d
8 oa3to4.oa3 . . 3 (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))
92, 4, 5, 6, 7, 8oa3to4lem6 950 . 2 ((ba) ∩ (dc)) ≤ (b ∪ (a ∩ (c ∪ ((bd) ∩ (ac)))))
109oa3to4lem5 949 1 ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((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: (None)
 Copyright terms: Public domain W3C validator