Metamath Proof Explorer

Theorem ldepsprlem

Description: Lemma for ldepspr . (Contributed by AV, 16-Apr-2019)

Ref Expression
Hypotheses snlindsntor.b 
|- B = ( Base ` M )
snlindsntor.r 
|- R = ( Scalar ` M )
snlindsntor.s 
|- S = ( Base ` R )
snlindsntor.0 
|- .0. = ( 0g ` R )
snlindsntor.z 
|- Z = ( 0g ` M )
snlindsntor.t 
|- .x. = ( .s ` M )
ldepsprlem.1 
|- .1. = ( 1r ` R )
ldepsprlem.n 
|- N = ( invg ` R )
Assertion ldepsprlem 
|- ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( X = ( A .x. Y ) -> ( ( .1. .x. X ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = Z ) )

Proof

Step Hyp Ref Expression
1 snlindsntor.b 
 |-  B = ( Base ` M )
2 snlindsntor.r 
 |-  R = ( Scalar ` M )
3 snlindsntor.s 
 |-  S = ( Base ` R )
4 snlindsntor.0 
 |-  .0. = ( 0g ` R )
5 snlindsntor.z 
 |-  Z = ( 0g ` M )
6 snlindsntor.t 
 |-  .x. = ( .s ` M )
7 ldepsprlem.1 
 |-  .1. = ( 1r ` R )
8 ldepsprlem.n 
 |-  N = ( invg ` R )
9 oveq2 
 |-  ( X = ( A .x. Y ) -> ( .1. .x. X ) = ( .1. .x. ( A .x. Y ) ) )
10 9 oveq1d 
 |-  ( X = ( A .x. Y ) -> ( ( .1. .x. X ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = ( ( .1. .x. ( A .x. Y ) ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) )
11 simpl 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> M e. LMod )
12 2 3 7 lmod1cl 
 |-  ( M e. LMod -> .1. e. S )
13 12 adantr 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> .1. e. S )
14 simpr3 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> A e. S )
15 simpr2 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> Y e. B )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 1 2 6 3 16 lmodvsass 
 |-  ( ( M e. LMod /\ ( .1. e. S /\ A e. S /\ Y e. B ) ) -> ( ( .1. ( .r ` R ) A ) .x. Y ) = ( .1. .x. ( A .x. Y ) ) )
18 11 13 14 15 17 syl13anc 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( .1. ( .r ` R ) A ) .x. Y ) = ( .1. .x. ( A .x. Y ) ) )
19 18 eqcomd 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( .1. .x. ( A .x. Y ) ) = ( ( .1. ( .r ` R ) A ) .x. Y ) )
20 19 oveq1d 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( .1. .x. ( A .x. Y ) ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = ( ( ( .1. ( .r ` R ) A ) .x. Y ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) )
21 2 lmodring 
 |-  ( M e. LMod -> R e. Ring )
22 simp3 
 |-  ( ( X e. B /\ Y e. B /\ A e. S ) -> A e. S )
23 3 16 7 ringlidm 
 |-  ( ( R e. Ring /\ A e. S ) -> ( .1. ( .r ` R ) A ) = A )
24 21 22 23 syl2an 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( .1. ( .r ` R ) A ) = A )
25 24 oveq1d 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( .1. ( .r ` R ) A ) .x. Y ) = ( A .x. Y ) )
26 25 oveq1d 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( ( .1. ( .r ` R ) A ) .x. Y ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = ( ( A .x. Y ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) )
27 2 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
28 3 8 grpinvcl 
 |-  ( ( R e. Grp /\ A e. S ) -> ( N ` A ) e. S )
29 27 22 28 syl2an 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( N ` A ) e. S )
30 eqid 
 |-  ( +g ` M ) = ( +g ` M )
31 eqid 
 |-  ( +g ` R ) = ( +g ` R )
32 1 30 2 6 3 31 lmodvsdir 
 |-  ( ( M e. LMod /\ ( A e. S /\ ( N ` A ) e. S /\ Y e. B ) ) -> ( ( A ( +g ` R ) ( N ` A ) ) .x. Y ) = ( ( A .x. Y ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) )
33 11 14 29 15 32 syl13anc 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( A ( +g ` R ) ( N ` A ) ) .x. Y ) = ( ( A .x. Y ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) )
34 3 31 4 8 grprinv 
 |-  ( ( R e. Grp /\ A e. S ) -> ( A ( +g ` R ) ( N ` A ) ) = .0. )
35 27 22 34 syl2an 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( A ( +g ` R ) ( N ` A ) ) = .0. )
36 35 oveq1d 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( A ( +g ` R ) ( N ` A ) ) .x. Y ) = ( .0. .x. Y ) )
37 1 2 6 4 5 lmod0vs 
 |-  ( ( M e. LMod /\ Y e. B ) -> ( .0. .x. Y ) = Z )
38 37 3ad2antr2 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( .0. .x. Y ) = Z )
39 36 38 eqtrd 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( A ( +g ` R ) ( N ` A ) ) .x. Y ) = Z )
40 26 33 39 3eqtr2d 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( ( .1. ( .r ` R ) A ) .x. Y ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = Z )
41 20 40 eqtrd 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( ( .1. .x. ( A .x. Y ) ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = Z )
42 10 41 sylan9eqr 
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) /\ X = ( A .x. Y ) ) -> ( ( .1. .x. X ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = Z )
43 42 ex 
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( X = ( A .x. Y ) -> ( ( .1. .x. X ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = Z ) )