Metamath Proof Explorer

Theorem latmassOLD

Description: Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) ( inass analog.) (Contributed by NM, 7-Nov-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses olmass.b 
|- B = ( Base ` K )
olmass.m 
|- ./\ = ( meet ` K )
Assertion latmassOLD 
|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )

Proof

Step Hyp Ref Expression
1 olmass.b 
 |-  B = ( Base ` K )
2 olmass.m 
 |-  ./\ = ( meet ` K )
3 simpl 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OL )
4 ollat 
 |-  ( K e. OL -> K e. Lat )
5 4 adantr 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
6 olop 
 |-  ( K e. OL -> K e. OP )
7 6 adantr 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OP )
8 simpr1 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
9 eqid 
 |-  ( oc ` K ) = ( oc ` K )
10 1 9 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
11 7 8 10 syl2anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` X ) e. B )
12 simpr2 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
13 1 9 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
14 7 12 13 syl2anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Y ) e. B )
15 eqid 
 |-  ( join ` K ) = ( join ` K )
16 1 15 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) e. B )
17 5 11 14 16 syl3anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) e. B )
18 simpr3 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
19 1 15 2 9 oldmj3 
 |-  ( ( K e. OL /\ ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) ./\ Z ) )
20 3 17 18 19 syl3anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) ./\ Z ) )
21 1 9 opoccl 
 |-  ( ( K e. OP /\ Z e. B ) -> ( ( oc ` K ) ` Z ) e. B )
22 7 18 21 syl2anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Z ) e. B )
23 1 15 latjass 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) )
24 5 11 14 22 23 syl13anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) )
25 24 fveq2d 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )
26 1 15 2 9 oldmj4 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X ./\ Y ) )
27 26 3adant3r3 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X ./\ Y ) )
28 27 oveq1d 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) ./\ Z ) = ( ( X ./\ Y ) ./\ Z ) )
29 20 25 28 3eqtr3rd 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )
30 1 15 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) e. B )
31 5 14 22 30 syl3anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) e. B )
32 1 15 2 9 oldmj2 
 |-  ( ( K e. OL /\ X e. B /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )
33 3 8 31 32 syl3anc 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )
34 1 15 2 9 oldmj4 
 |-  ( ( K e. OL /\ Y e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( Y ./\ Z ) )
35 34 3adant3r1 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( Y ./\ Z ) )
36 35 oveq2d 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( Y ./\ Z ) ) )
37 29 33 36 3eqtrd 
 |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )