Proof of Theorem ldepsprlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . 4
⊢ (𝑋 = (𝐴 · 𝑌) → ( 1 · 𝑋) = ( 1 · (𝐴 · 𝑌))) | 
| 2 | 1 | oveq1d 7446 | . . 3
⊢ (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = (( 1 · (𝐴 · 𝑌))(+g‘𝑀)((𝑁‘𝐴) · 𝑌))) | 
| 3 |  | simpl 482 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → 𝑀 ∈ LMod) | 
| 4 |  | snlindsntor.r | . . . . . . . . 9
⊢ 𝑅 = (Scalar‘𝑀) | 
| 5 |  | snlindsntor.s | . . . . . . . . 9
⊢ 𝑆 = (Base‘𝑅) | 
| 6 |  | ldepsprlem.1 | . . . . . . . . 9
⊢  1 =
(1r‘𝑅) | 
| 7 | 4, 5, 6 | lmod1cl 20887 | . . . . . . . 8
⊢ (𝑀 ∈ LMod → 1 ∈ 𝑆) | 
| 8 | 7 | adantr 480 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → 1 ∈ 𝑆) | 
| 9 |  | simpr3 1197 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → 𝐴 ∈ 𝑆) | 
| 10 |  | simpr2 1196 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → 𝑌 ∈ 𝐵) | 
| 11 |  | snlindsntor.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝑀) | 
| 12 |  | snlindsntor.t | . . . . . . . 8
⊢  · = (
·𝑠 ‘𝑀) | 
| 13 |  | eqid 2737 | . . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 14 | 11, 4, 12, 5, 13 | lmodvsass 20885 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ ( 1 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝐵)) → (( 1 (.r‘𝑅)𝐴) · 𝑌) = ( 1 · (𝐴 · 𝑌))) | 
| 15 | 3, 8, 9, 10, 14 | syl13anc 1374 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (( 1 (.r‘𝑅)𝐴) · 𝑌) = ( 1 · (𝐴 · 𝑌))) | 
| 16 | 15 | eqcomd 2743 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ( 1 · (𝐴 · 𝑌)) = (( 1 (.r‘𝑅)𝐴) · 𝑌)) | 
| 17 | 16 | oveq1d 7446 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (( 1 · (𝐴 · 𝑌))(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = ((( 1 (.r‘𝑅)𝐴) · 𝑌)(+g‘𝑀)((𝑁‘𝐴) · 𝑌))) | 
| 18 | 4 | lmodring 20866 | . . . . . . . 8
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Ring) | 
| 19 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆) → 𝐴 ∈ 𝑆) | 
| 20 | 5, 13, 6 | ringlidm 20266 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑆) → ( 1 (.r‘𝑅)𝐴) = 𝐴) | 
| 21 | 18, 19, 20 | syl2an 596 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ( 1 (.r‘𝑅)𝐴) = 𝐴) | 
| 22 | 21 | oveq1d 7446 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (( 1 (.r‘𝑅)𝐴) · 𝑌) = (𝐴 · 𝑌)) | 
| 23 | 22 | oveq1d 7446 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ((( 1 (.r‘𝑅)𝐴) · 𝑌)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = ((𝐴 · 𝑌)(+g‘𝑀)((𝑁‘𝐴) · 𝑌))) | 
| 24 | 4 | lmodfgrp 20867 | . . . . . . 7
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Grp) | 
| 25 |  | ldepsprlem.n | . . . . . . . 8
⊢ 𝑁 = (invg‘𝑅) | 
| 26 | 5, 25 | grpinvcl 19005 | . . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑆) → (𝑁‘𝐴) ∈ 𝑆) | 
| 27 | 24, 19, 26 | syl2an 596 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑁‘𝐴) ∈ 𝑆) | 
| 28 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 29 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 30 | 11, 28, 4, 12, 5, 29 | lmodvsdir 20884 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝐴 ∈ 𝑆 ∧ (𝑁‘𝐴) ∈ 𝑆 ∧ 𝑌 ∈ 𝐵)) → ((𝐴(+g‘𝑅)(𝑁‘𝐴)) · 𝑌) = ((𝐴 · 𝑌)(+g‘𝑀)((𝑁‘𝐴) · 𝑌))) | 
| 31 | 3, 9, 27, 10, 30 | syl13anc 1374 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ((𝐴(+g‘𝑅)(𝑁‘𝐴)) · 𝑌) = ((𝐴 · 𝑌)(+g‘𝑀)((𝑁‘𝐴) · 𝑌))) | 
| 32 |  | snlindsntor.0 | . . . . . . . . 9
⊢  0 =
(0g‘𝑅) | 
| 33 | 5, 29, 32, 25 | grprinv 19008 | . . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑆) → (𝐴(+g‘𝑅)(𝑁‘𝐴)) = 0 ) | 
| 34 | 24, 19, 33 | syl2an 596 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝐴(+g‘𝑅)(𝑁‘𝐴)) = 0 ) | 
| 35 | 34 | oveq1d 7446 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ((𝐴(+g‘𝑅)(𝑁‘𝐴)) · 𝑌) = ( 0 · 𝑌)) | 
| 36 |  | snlindsntor.z | . . . . . . . 8
⊢ 𝑍 = (0g‘𝑀) | 
| 37 | 11, 4, 12, 32, 36 | lmod0vs 20893 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵) → ( 0 · 𝑌) = 𝑍) | 
| 38 | 37 | 3ad2antr2 1190 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ( 0 · 𝑌) = 𝑍) | 
| 39 | 35, 38 | eqtrd 2777 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ((𝐴(+g‘𝑅)(𝑁‘𝐴)) · 𝑌) = 𝑍) | 
| 40 | 23, 31, 39 | 3eqtr2d 2783 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → ((( 1 (.r‘𝑅)𝐴) · 𝑌)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍) | 
| 41 | 17, 40 | eqtrd 2777 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (( 1 · (𝐴 · 𝑌))(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍) | 
| 42 | 2, 41 | sylan9eqr 2799 | . 2
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) ∧ 𝑋 = (𝐴 · 𝑌)) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍) | 
| 43 | 42 | ex 412 | 1
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍)) |