Metamath Proof Explorer

Theorem ldepsprlem

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

Ref Expression
Hypotheses snlindsntor.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
snlindsntor.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
snlindsntor.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
snlindsntor.0 ⊢ 0 = ( 0g ‘ 𝑅 )
snlindsntor.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
snlindsntor.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
ldepsprlem.1 ⊢ 1 = ( 1r ‘ 𝑅 )
ldepsprlem.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
Assertion ldepsprlem ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 snlindsntor.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 snlindsntor.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 snlindsntor.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
4 snlindsntor.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 snlindsntor.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
6 snlindsntor.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
7 ldepsprlem.1 ⊢ 1 = ( 1r ‘ 𝑅 )
8 ldepsprlem.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
9 oveq2 ⊢ ( 𝑋 = ( 𝐴 · 𝑌 ) → ( 1 · 𝑋 ) = ( 1 · ( 𝐴 · 𝑌 ) ) )
10 9 oveq1d ⊢ ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = ( ( 1 · ( 𝐴 · 𝑌 ) ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
11 simpl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → 𝑀 ∈ LMod )
12 2 3 7 lmod1cl ⊢ ( 𝑀 ∈ LMod → 1 ∈ 𝑆 )
13 12 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → 1 ∈ 𝑆 )
14 simpr3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → 𝐴 ∈ 𝑆 )
15 simpr2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → 𝑌 ∈ 𝐵 )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 1 2 6 3 16 lmodvsass ⊢ ( ( 𝑀 ∈ LMod ∧ ( 1 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) = ( 1 · ( 𝐴 · 𝑌 ) ) )
18 11 13 14 15 17 syl13anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) = ( 1 · ( 𝐴 · 𝑌 ) ) )
19 18 eqcomd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 1 · ( 𝐴 · 𝑌 ) ) = ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) )
20 19 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 1 · ( 𝐴 · 𝑌 ) ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = ( ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
21 2 lmodring ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Ring )
22 simp3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
23 3 16 7 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑆 ) → ( 1 ( .r ‘ 𝑅 ) 𝐴 ) = 𝐴 )
24 21 22 23 syl2an ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 1 ( .r ‘ 𝑅 ) 𝐴 ) = 𝐴 )
25 24 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) = ( 𝐴 · 𝑌 ) )
26 25 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = ( ( 𝐴 · 𝑌 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
27 2 lmodfgrp ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
28 3 8 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑆 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 )
29 27 22 28 syl2an ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 )
30 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
31 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
32 1 30 2 6 3 31 lmodvsdir ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐴 ∈ 𝑆 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐴 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = ( ( 𝐴 · 𝑌 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
33 11 14 29 15 32 syl13anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 𝐴 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = ( ( 𝐴 · 𝑌 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
34 3 31 4 8 grprinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) = 0 )
35 27 22 34 syl2an ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 𝐴 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) = 0 )
36 35 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 𝐴 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = ( 0 · 𝑌 ) )
37 1 2 6 4 5 lmod0vs ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) → ( 0 · 𝑌 ) = 𝑍 )
38 37 3ad2antr2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 0 · 𝑌 ) = 𝑍 )
39 36 38 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 𝐴 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝐴 ) ) · 𝑌 ) = 𝑍 )
40 26 33 39 3eqtr2d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 1 ( .r ‘ 𝑅 ) 𝐴 ) · 𝑌 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 )
41 20 40 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( 1 · ( 𝐴 · 𝑌 ) ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 )
42 10 41 sylan9eqr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 )
43 42 ex ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 1 · 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 ) )