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

Theorem omlfh3N 34349
 Description: Foulis-Holland Theorem, part 3. Dual of omlfh1N 34348. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlfh1.b
omlfh1.j
omlfh1.m
omlfh1.c
Assertion
Ref Expression
omlfh3N

Proof of Theorem omlfh3N
StepHypRef Expression
1 omlfh1.b . . . . . . 7
2 eqid 2467 . . . . . . 7
3 omlfh1.c . . . . . . 7
41, 2, 3cmt4N 34342 . . . . . 6
543adant3r3 1207 . . . . 5
61, 2, 3cmt4N 34342 . . . . . 6
763adant3r2 1206 . . . . 5
85, 7anbi12d 710 . . . 4
9 simpl 457 . . . . 5
10 omlop 34331 . . . . . . . 8
1110adantr 465 . . . . . . 7
12 simpr1 1002 . . . . . . 7
131, 2opoccl 34284 . . . . . . 7
1411, 12, 13syl2anc 661 . . . . . 6
15 simpr2 1003 . . . . . . 7
161, 2opoccl 34284 . . . . . . 7
1711, 15, 16syl2anc 661 . . . . . 6
18 simpr3 1004 . . . . . . 7
191, 2opoccl 34284 . . . . . . 7
2011, 18, 19syl2anc 661 . . . . . 6
2114, 17, 203jca 1176 . . . . 5
22 omlfh1.j . . . . . . . 8
23 omlfh1.m . . . . . . . 8
241, 22, 23, 3omlfh1N 34348 . . . . . . 7
2524fveq2d 5875 . . . . . 6
26253exp 1195 . . . . 5
279, 21, 26sylc 60 . . . 4
288, 27sylbid 215 . . 3
29283impia 1193 . 2
30 omlol 34330 . . . . . 6
3130adantr 465 . . . . 5
32 omllat 34332 . . . . . . 7
3332adantr 465 . . . . . 6
341, 22latjcl 15550 . . . . . 6
3533, 17, 20, 34syl3anc 1228 . . . . 5
361, 22, 23, 2oldmm2 34308 . . . . 5
3731, 12, 35, 36syl3anc 1228 . . . 4
381, 22, 23, 2oldmj4 34314 . . . . . 6
3931, 15, 18, 38syl3anc 1228 . . . . 5
4039oveq2d 6310 . . . 4
4137, 40eqtr2d 2509 . . 3
431, 23latmcl 15551 . . . . . 6
4433, 14, 17, 43syl3anc 1228 . . . . 5
451, 23latmcl 15551 . . . . . 6
4633, 14, 20, 45syl3anc 1228 . . . . 5
471, 22, 23, 2oldmj1 34311 . . . . 5
4831, 44, 46, 47syl3anc 1228 . . . 4
491, 22, 23, 2oldmm4 34310 . . . . . 6
5031, 12, 15, 49syl3anc 1228 . . . . 5
511, 22, 23, 2oldmm4 34310 . . . . . 6
5231, 12, 18, 51syl3anc 1228 . . . . 5
5350, 52oveq12d 6312 . . . 4
5448, 53eqtr2d 2509 . . 3