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

Theorem latmassOLD 29712
 Description: Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 3511 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
olmass.b
olmass.m
Assertion
Ref Expression
latmassOLD

Proof of Theorem latmassOLD
StepHypRef Expression
1 simpl 444 . . . 4
2 ollat 29696 . . . . . 6
32adantr 452 . . . . 5
4 olop 29697 . . . . . . 7
54adantr 452 . . . . . 6
6 simpr1 963 . . . . . 6
7 olmass.b . . . . . . 7
8 eqid 2404 . . . . . . 7
97, 8opoccl 29677 . . . . . 6
105, 6, 9syl2anc 643 . . . . 5
11 simpr2 964 . . . . . 6
127, 8opoccl 29677 . . . . . 6
135, 11, 12syl2anc 643 . . . . 5
14 eqid 2404 . . . . . 6
157, 14latjcl 14434 . . . . 5
163, 10, 13, 15syl3anc 1184 . . . 4
17 simpr3 965 . . . 4
18 olmass.m . . . . 5
197, 14, 18, 8oldmj3 29706 . . . 4
201, 16, 17, 19syl3anc 1184 . . 3
217, 8opoccl 29677 . . . . . 6
225, 17, 21syl2anc 643 . . . . 5
237, 14latjass 14479 . . . . 5
243, 10, 13, 22, 23syl13anc 1186 . . . 4
2524fveq2d 5691 . . 3
267, 14, 18, 8oldmj4 29707 . . . . 5
27263adant3r3 1164 . . . 4
2827oveq1d 6055 . . 3
2920, 25, 283eqtr3rd 2445 . 2
307, 14latjcl 14434 . . . 4
313, 13, 22, 30syl3anc 1184 . . 3
327, 14, 18, 8oldmj2 29705 . . 3
331, 6, 31, 32syl3anc 1184 . 2
347, 14, 18, 8oldmj4 29707 . . . 4