Metamath Proof Explorer

Theorem latdisdlem

Description: Lemma for latdisd . (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses latdisd.b 
|- B = ( Base ` K )
latdisd.j 
|- .\/ = ( join ` K )
latdisd.m 
|- ./\ = ( meet ` K )
Assertion latdisdlem 
|- ( K e. Lat -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )

Proof

Step Hyp Ref Expression
1 latdisd.b 
 |-  B = ( Base ` K )
2 latdisd.j 
 |-  .\/ = ( join ` K )
3 latdisd.m 
 |-  ./\ = ( meet ` K )
4 1 3 latmcl 
 |-  ( ( K e. Lat /\ x e. B /\ y e. B ) -> ( x ./\ y ) e. B )
5 4 3adant3r3 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ./\ y ) e. B )
6 simpr1 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> x e. B )
7 simpr3 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> z e. B )
8 oveq1 
 |-  ( u = ( x ./\ y ) -> ( u .\/ ( v ./\ w ) ) = ( ( x ./\ y ) .\/ ( v ./\ w ) ) )
9 oveq1 
 |-  ( u = ( x ./\ y ) -> ( u .\/ v ) = ( ( x ./\ y ) .\/ v ) )
10 oveq1 
 |-  ( u = ( x ./\ y ) -> ( u .\/ w ) = ( ( x ./\ y ) .\/ w ) )
11 9 10 oveq12d 
 |-  ( u = ( x ./\ y ) -> ( ( u .\/ v ) ./\ ( u .\/ w ) ) = ( ( ( x ./\ y ) .\/ v ) ./\ ( ( x ./\ y ) .\/ w ) ) )
12 8 11 eqeq12d 
 |-  ( u = ( x ./\ y ) -> ( ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) <-> ( ( x ./\ y ) .\/ ( v ./\ w ) ) = ( ( ( x ./\ y ) .\/ v ) ./\ ( ( x ./\ y ) .\/ w ) ) ) )
13 oveq1 
 |-  ( v = x -> ( v ./\ w ) = ( x ./\ w ) )
14 13 oveq2d 
 |-  ( v = x -> ( ( x ./\ y ) .\/ ( v ./\ w ) ) = ( ( x ./\ y ) .\/ ( x ./\ w ) ) )
15 oveq2 
 |-  ( v = x -> ( ( x ./\ y ) .\/ v ) = ( ( x ./\ y ) .\/ x ) )
16 15 oveq1d 
 |-  ( v = x -> ( ( ( x ./\ y ) .\/ v ) ./\ ( ( x ./\ y ) .\/ w ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ w ) ) )
17 14 16 eqeq12d 
 |-  ( v = x -> ( ( ( x ./\ y ) .\/ ( v ./\ w ) ) = ( ( ( x ./\ y ) .\/ v ) ./\ ( ( x ./\ y ) .\/ w ) ) <-> ( ( x ./\ y ) .\/ ( x ./\ w ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ w ) ) ) )
18 oveq2 
 |-  ( w = z -> ( x ./\ w ) = ( x ./\ z ) )
19 18 oveq2d 
 |-  ( w = z -> ( ( x ./\ y ) .\/ ( x ./\ w ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
20 oveq2 
 |-  ( w = z -> ( ( x ./\ y ) .\/ w ) = ( ( x ./\ y ) .\/ z ) )
21 20 oveq2d 
 |-  ( w = z -> ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ w ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) )
22 19 21 eqeq12d 
 |-  ( w = z -> ( ( ( x ./\ y ) .\/ ( x ./\ w ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ w ) ) <-> ( ( x ./\ y ) .\/ ( x ./\ z ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) ) )
23 12 17 22 rspc3v 
 |-  ( ( ( x ./\ y ) e. B /\ x e. B /\ z e. B ) -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> ( ( x ./\ y ) .\/ ( x ./\ z ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) ) )
24 5 6 7 23 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> ( ( x ./\ y ) .\/ ( x ./\ z ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) ) )
25 24 imp 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( ( x ./\ y ) .\/ ( x ./\ z ) ) = ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) )
26 simpl 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> K e. Lat )
27 1 2 latjcom 
 |-  ( ( K e. Lat /\ ( x ./\ y ) e. B /\ x e. B ) -> ( ( x ./\ y ) .\/ x ) = ( x .\/ ( x ./\ y ) ) )
28 26 5 6 27 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ./\ y ) .\/ x ) = ( x .\/ ( x ./\ y ) ) )
29 1 2 3 latabs1 
 |-  ( ( K e. Lat /\ x e. B /\ y e. B ) -> ( x .\/ ( x ./\ y ) ) = x )
30 29 3adant3r3 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .\/ ( x ./\ y ) ) = x )
31 28 30 eqtrd 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ./\ y ) .\/ x ) = x )
32 1 2 latjcom 
 |-  ( ( K e. Lat /\ ( x ./\ y ) e. B /\ z e. B ) -> ( ( x ./\ y ) .\/ z ) = ( z .\/ ( x ./\ y ) ) )
33 26 5 7 32 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ./\ y ) .\/ z ) = ( z .\/ ( x ./\ y ) ) )
34 31 33 oveq12d 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) = ( x ./\ ( z .\/ ( x ./\ y ) ) ) )
35 34 adantr 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( ( ( x ./\ y ) .\/ x ) ./\ ( ( x ./\ y ) .\/ z ) ) = ( x ./\ ( z .\/ ( x ./\ y ) ) ) )
36 simpr2 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> y e. B )
37 oveq1 
 |-  ( u = z -> ( u .\/ ( v ./\ w ) ) = ( z .\/ ( v ./\ w ) ) )
38 oveq1 
 |-  ( u = z -> ( u .\/ v ) = ( z .\/ v ) )
39 oveq1 
 |-  ( u = z -> ( u .\/ w ) = ( z .\/ w ) )
40 38 39 oveq12d 
 |-  ( u = z -> ( ( u .\/ v ) ./\ ( u .\/ w ) ) = ( ( z .\/ v ) ./\ ( z .\/ w ) ) )
41 37 40 eqeq12d 
 |-  ( u = z -> ( ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) <-> ( z .\/ ( v ./\ w ) ) = ( ( z .\/ v ) ./\ ( z .\/ w ) ) ) )
42 13 oveq2d 
 |-  ( v = x -> ( z .\/ ( v ./\ w ) ) = ( z .\/ ( x ./\ w ) ) )
43 oveq2 
 |-  ( v = x -> ( z .\/ v ) = ( z .\/ x ) )
44 43 oveq1d 
 |-  ( v = x -> ( ( z .\/ v ) ./\ ( z .\/ w ) ) = ( ( z .\/ x ) ./\ ( z .\/ w ) ) )
45 42 44 eqeq12d 
 |-  ( v = x -> ( ( z .\/ ( v ./\ w ) ) = ( ( z .\/ v ) ./\ ( z .\/ w ) ) <-> ( z .\/ ( x ./\ w ) ) = ( ( z .\/ x ) ./\ ( z .\/ w ) ) ) )
46 oveq2 
 |-  ( w = y -> ( x ./\ w ) = ( x ./\ y ) )
47 46 oveq2d 
 |-  ( w = y -> ( z .\/ ( x ./\ w ) ) = ( z .\/ ( x ./\ y ) ) )
48 oveq2 
 |-  ( w = y -> ( z .\/ w ) = ( z .\/ y ) )
49 48 oveq2d 
 |-  ( w = y -> ( ( z .\/ x ) ./\ ( z .\/ w ) ) = ( ( z .\/ x ) ./\ ( z .\/ y ) ) )
50 47 49 eqeq12d 
 |-  ( w = y -> ( ( z .\/ ( x ./\ w ) ) = ( ( z .\/ x ) ./\ ( z .\/ w ) ) <-> ( z .\/ ( x ./\ y ) ) = ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) )
51 41 45 50 rspc3v 
 |-  ( ( z e. B /\ x e. B /\ y e. B ) -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> ( z .\/ ( x ./\ y ) ) = ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) )
52 7 6 36 51 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> ( z .\/ ( x ./\ y ) ) = ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) )
53 52 imp 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( z .\/ ( x ./\ y ) ) = ( ( z .\/ x ) ./\ ( z .\/ y ) ) )
54 53 oveq2d 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( x ./\ ( z .\/ ( x ./\ y ) ) ) = ( x ./\ ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) )
55 1 2 latjcl 
 |-  ( ( K e. Lat /\ z e. B /\ x e. B ) -> ( z .\/ x ) e. B )
56 26 7 6 55 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( z .\/ x ) e. B )
57 1 2 latjcl 
 |-  ( ( K e. Lat /\ z e. B /\ y e. B ) -> ( z .\/ y ) e. B )
58 26 7 36 57 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( z .\/ y ) e. B )
59 1 3 latmass 
 |-  ( ( K e. Lat /\ ( x e. B /\ ( z .\/ x ) e. B /\ ( z .\/ y ) e. B ) ) -> ( ( x ./\ ( z .\/ x ) ) ./\ ( z .\/ y ) ) = ( x ./\ ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) )
60 26 6 56 58 59 syl13anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ./\ ( z .\/ x ) ) ./\ ( z .\/ y ) ) = ( x ./\ ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) )
61 1 2 latjcom 
 |-  ( ( K e. Lat /\ z e. B /\ x e. B ) -> ( z .\/ x ) = ( x .\/ z ) )
62 26 7 6 61 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( z .\/ x ) = ( x .\/ z ) )
63 62 oveq2d 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ./\ ( z .\/ x ) ) = ( x ./\ ( x .\/ z ) ) )
64 1 2 3 latabs2 
 |-  ( ( K e. Lat /\ x e. B /\ z e. B ) -> ( x ./\ ( x .\/ z ) ) = x )
65 26 6 7 64 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ./\ ( x .\/ z ) ) = x )
66 63 65 eqtrd 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ./\ ( z .\/ x ) ) = x )
67 1 2 latjcom 
 |-  ( ( K e. Lat /\ z e. B /\ y e. B ) -> ( z .\/ y ) = ( y .\/ z ) )
68 26 7 36 67 syl3anc 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( z .\/ y ) = ( y .\/ z ) )
69 66 68 oveq12d 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ./\ ( z .\/ x ) ) ./\ ( z .\/ y ) ) = ( x ./\ ( y .\/ z ) ) )
70 60 69 eqtr3d 
 |-  ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ./\ ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) = ( x ./\ ( y .\/ z ) ) )
71 70 adantr 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( x ./\ ( ( z .\/ x ) ./\ ( z .\/ y ) ) ) = ( x ./\ ( y .\/ z ) ) )
72 54 71 eqtrd 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( x ./\ ( z .\/ ( x ./\ y ) ) ) = ( x ./\ ( y .\/ z ) ) )
73 25 35 72 3eqtrrd 
 |-  ( ( ( K e. Lat /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
74 73 an32s 
 |-  ( ( ( K e. Lat /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
75 74 ralrimivvva 
 |-  ( ( K e. Lat /\ A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) ) -> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
76 75 ex 
 |-  ( K e. Lat -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )