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

Theorem latmassOLD 30028
 Description: Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 3552 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 445 . . . 4
2 ollat 30012 . . . . . 6
32adantr 453 . . . . 5
4 olop 30013 . . . . . . 7
54adantr 453 . . . . . 6
6 simpr1 964 . . . . . 6
7 olmass.b . . . . . . 7
8 eqid 2437 . . . . . . 7
97, 8opoccl 29993 . . . . . 6
105, 6, 9syl2anc 644 . . . . 5
11 simpr2 965 . . . . . 6
127, 8opoccl 29993 . . . . . 6
135, 11, 12syl2anc 644 . . . . 5
14 eqid 2437 . . . . . 6
157, 14latjcl 14480 . . . . 5
163, 10, 13, 15syl3anc 1185 . . . 4
17 simpr3 966 . . . 4
18 olmass.m . . . . 5
197, 14, 18, 8oldmj3 30022 . . . 4
201, 16, 17, 19syl3anc 1185 . . 3
217, 8opoccl 29993 . . . . . 6
225, 17, 21syl2anc 644 . . . . 5
237, 14latjass 14525 . . . . 5
243, 10, 13, 22, 23syl13anc 1187 . . . 4
2524fveq2d 5733 . . 3
267, 14, 18, 8oldmj4 30023 . . . . 5
27263adant3r3 1165 . . . 4
2827oveq1d 6097 . . 3
2920, 25, 283eqtr3rd 2478 . 2
307, 14latjcl 14480 . . . 4
313, 13, 22, 30syl3anc 1185 . . 3
327, 14, 18, 8oldmj2 30021 . . 3
331, 6, 31, 32syl3anc 1185 . 2
347, 14, 18, 8oldmj4 30023 . . . 4