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 ) ) ) |