Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omlfh1N Unicode version

Theorem omlfh1N 28137
 Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in [Kalmbach] p. 25. (fh1 22045 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlfh1.b
omlfh1.j
omlfh1.m
omlfh1.c
Assertion
Ref Expression
omlfh1N

Proof of Theorem omlfh1N
StepHypRef Expression
1 omllat 28121 . . . . 5
2 omlfh1.b . . . . . 6
3 eqid 2253 . . . . . 6
4 omlfh1.j . . . . . 6
5 omlfh1.m . . . . . 6
62, 3, 4, 5latledi 14039 . . . . 5
71, 6sylan 459 . . . 4
91adantr 453 . . . . . . 7
10 simpr1 966 . . . . . . 7
11 simpr2 967 . . . . . . . 8
12 simpr3 968 . . . . . . . 8
132, 4latjcl 14000 . . . . . . . 8
149, 11, 12, 13syl3anc 1187 . . . . . . 7
152, 5latmcom 14025 . . . . . . 7
169, 10, 14, 15syl3anc 1187 . . . . . 6
17 omlol 28119 . . . . . . . . 9
1817adantr 453 . . . . . . . 8
192, 5latmcl 14001 . . . . . . . . 9
209, 10, 11, 19syl3anc 1187 . . . . . . . 8
212, 5latmcl 14001 . . . . . . . . 9
229, 10, 12, 21syl3anc 1187 . . . . . . . 8
23 eqid 2253 . . . . . . . . 9
242, 4, 5, 23oldmj1 28100 . . . . . . . 8
2518, 20, 22, 24syl3anc 1187 . . . . . . 7
262, 4, 5, 23oldmm1 28096 . . . . . . . . 9
2718, 10, 11, 26syl3anc 1187 . . . . . . . 8
282, 4, 5, 23oldmm1 28096 . . . . . . . . 9
2918, 10, 12, 28syl3anc 1187 . . . . . . . 8
3027, 29oveq12d 5728 . . . . . . 7
3125, 30eqtrd 2285 . . . . . 6
3216, 31oveq12d 5728 . . . . 5
33323adant3 980 . . . 4
34 omlop 28120 . . . . . . . . . . 11
3534adantr 453 . . . . . . . . . 10
362, 23opoccl 28073 . . . . . . . . . 10
3735, 10, 36syl2anc 645 . . . . . . . . 9
382, 23opoccl 28073 . . . . . . . . . 10
3935, 11, 38syl2anc 645 . . . . . . . . 9
402, 4latjcl 14000 . . . . . . . . 9
419, 37, 39, 40syl3anc 1187 . . . . . . . 8
422, 23opoccl 28073 . . . . . . . . . 10
4335, 12, 42syl2anc 645 . . . . . . . . 9
442, 4latjcl 14000 . . . . . . . . 9
459, 37, 43, 44syl3anc 1187 . . . . . . . 8
462, 5latmcl 14001 . . . . . . . 8
479, 41, 45, 46syl3anc 1187 . . . . . . 7
482, 5latmassOLD 28108 . . . . . . 7
4918, 14, 10, 47, 48syl13anc 1189 . . . . . 6
50493adant3 980 . . . . 5
51 omlfh1.c . . . . . . . . . . . . . 14
522, 23, 51cmt2N 28129 . . . . . . . . . . . . 13
53523adant3r3 1167 . . . . . . . . . . . 12
54 simpl 445 . . . . . . . . . . . . 13
552, 4, 5, 23, 51cmtbr3N 28133 . . . . . . . . . . . . 13
5654, 10, 39, 55syl3anc 1187 . . . . . . . . . . . 12
5753, 56bitrd 246 . . . . . . . . . . 11
5857biimpa 472 . . . . . . . . . 10
5958adantrr 700 . . . . . . . . 9
60593impa 1151 . . . . . . . 8
612, 23, 51cmt2N 28129 . . . . . . . . . . . . 13
62613adant3r2 1166 . . . . . . . . . . . 12
632, 4, 5, 23, 51cmtbr3N 28133 . . . . . . . . . . . . 13
6454, 10, 43, 63syl3anc 1187 . . . . . . . . . . . 12
6562, 64bitrd 246 . . . . . . . . . . 11
6665biimpa 472 . . . . . . . . . 10
6766adantrl 699 . . . . . . . . 9
68673impa 1151 . . . . . . . 8
6960, 68oveq12d 5728 . . . . . . 7
702, 5latmmdiN 28113 . . . . . . . . 9
7118, 10, 41, 45, 70syl13anc 1189 . . . . . . . 8
72713adant3 980 . . . . . . 7
732, 5latmmdiN 28113 . . . . . . . . 9
7418, 10, 39, 43, 73syl13anc 1189 . . . . . . . 8
75743adant3 980 . . . . . . 7
7669, 72, 753eqtr4d 2295 . . . . . 6
7776oveq2d 5726 . . . . 5
782, 5latmcl 14001 . . . . . . . 8
799, 39, 43, 78syl3anc 1187 . . . . . . 7
802, 5latm12 28109 . . . . . . 7
8118, 14, 10, 79, 80syl13anc 1189 . . . . . 6
82813adant3 980 . . . . 5
8350, 77, 823eqtrd 2289 . . . 4
842, 4, 5, 23oldmj1 28100 . . . . . . . . . 10
8518, 11, 12, 84syl3anc 1187 . . . . . . . . 9
8685oveq2d 5726 . . . . . . . 8
87 eqid 2253 . . . . . . . . . 10
882, 23, 5, 87opnoncon 28087 . . . . . . . . 9
8935, 14, 88syl2anc 645 . . . . . . . 8
9086, 89eqtr3d 2287 . . . . . . 7
9190oveq2d 5726 . . . . . 6
922, 5, 87olm01 28115 . . . . . . 7
9318, 10, 92syl2anc 645 . . . . . 6
9491, 93eqtrd 2285 . . . . 5
95943adant3 980 . . . 4
9633, 83, 953eqtrd 2289 . . 3
972, 4latjcl 14000 . . . . . 6
989, 20, 22, 97syl3anc 1187 . . . . 5
992, 5latmcl 14001 . . . . . 6
1009, 10, 14, 99syl3anc 1187 . . . . 5
1012, 3, 5, 23, 87omllaw3 28124 . . . . 5
10254, 98, 100, 101syl3anc 1187 . . . 4