| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑀 ∈ LMod) |
| 2 | | linc0scn0.s |
. . . . . . . . 9
⊢ 𝑆 = (Scalar‘𝑀) |
| 3 | 2 | lmodring 20866 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Ring) |
| 4 | 2 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑀) =
𝑆 |
| 5 | 4 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) |
| 6 | | linc0scn0.1 |
. . . . . . . . . 10
⊢ 1 =
(1r‘𝑆) |
| 7 | 5, 6 | ringidcl 20262 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring → 1 ∈
(Base‘(Scalar‘𝑀))) |
| 8 | | linc0scn0.0 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑆) |
| 9 | 5, 8 | ring0cl 20264 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring → 0 ∈
(Base‘(Scalar‘𝑀))) |
| 10 | 7, 9 | jca 511 |
. . . . . . . 8
⊢ (𝑆 ∈ Ring → ( 1 ∈
(Base‘(Scalar‘𝑀)) ∧ 0 ∈
(Base‘(Scalar‘𝑀)))) |
| 11 | 3, 10 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ LMod → ( 1 ∈
(Base‘(Scalar‘𝑀)) ∧ 0 ∈
(Base‘(Scalar‘𝑀)))) |
| 12 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑉) → ( 1 ∈
(Base‘(Scalar‘𝑀)) ∧ 0 ∈
(Base‘(Scalar‘𝑀)))) |
| 13 | | ifcl 4571 |
. . . . . 6
⊢ (( 1 ∈
(Base‘(Scalar‘𝑀)) ∧ 0 ∈
(Base‘(Scalar‘𝑀))) → if(𝑥 = 𝑍, 1 , 0 ) ∈
(Base‘(Scalar‘𝑀))) |
| 14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑉) → if(𝑥 = 𝑍, 1 , 0 ) ∈
(Base‘(Scalar‘𝑀))) |
| 15 | | linc0scn0.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑍, 1 , 0 )) |
| 16 | 14, 15 | fmptd 7134 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀))) |
| 17 | | fvex 6919 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
| 18 | 17 | a1i 11 |
. . . . 5
⊢ (𝑀 ∈ LMod →
(Base‘(Scalar‘𝑀)) ∈ V) |
| 19 | | elmapg 8879 |
. . . . 5
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) |
| 20 | 18, 19 | sylan 580 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) |
| 21 | 16, 20 | mpbird 257 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 22 | | linc0scn0.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
| 23 | 22 | pweqi 4616 |
. . . . . 6
⊢ 𝒫
𝐵 = 𝒫
(Base‘𝑀) |
| 24 | 23 | eleq2i 2833 |
. . . . 5
⊢ (𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 (Base‘𝑀)) |
| 25 | 24 | biimpi 216 |
. . . 4
⊢ (𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
| 26 | 25 | adantl 481 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
| 27 | | lincval 48326 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 28 | 1, 21, 26, 27 | syl3anc 1373 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 29 | | simpr 484 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
| 30 | 6 | fvexi 6920 |
. . . . . . . 8
⊢ 1 ∈
V |
| 31 | 8 | fvexi 6920 |
. . . . . . . 8
⊢ 0 ∈
V |
| 32 | 30, 31 | ifex 4576 |
. . . . . . 7
⊢ if(𝑣 = 𝑍, 1 , 0 ) ∈
V |
| 33 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑥 = 𝑍 ↔ 𝑣 = 𝑍)) |
| 34 | 33 | ifbid 4549 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑍, 1 , 0 ) = if(𝑣 = 𝑍, 1 , 0 )) |
| 35 | 34, 15 | fvmptg 7014 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑉 ∧ if(𝑣 = 𝑍, 1 , 0 ) ∈ V) → (𝐹‘𝑣) = if(𝑣 = 𝑍, 1 , 0 )) |
| 36 | 29, 32, 35 | sylancl 586 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) = if(𝑣 = 𝑍, 1 , 0 )) |
| 37 | 36 | oveq1d 7446 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = (if(𝑣 = 𝑍, 1 , 0 )(
·𝑠 ‘𝑀)𝑣)) |
| 38 | | ovif 7531 |
. . . . . 6
⊢ (if(𝑣 = 𝑍, 1 , 0 )(
·𝑠 ‘𝑀)𝑣) = if(𝑣 = 𝑍, ( 1 (
·𝑠 ‘𝑀)𝑣), ( 0 (
·𝑠 ‘𝑀)𝑣)) |
| 39 | 38 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑍, 1 , 0 )(
·𝑠 ‘𝑀)𝑣) = if(𝑣 = 𝑍, ( 1 (
·𝑠 ‘𝑀)𝑣), ( 0 (
·𝑠 ‘𝑀)𝑣))) |
| 40 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑣 = 𝑍 → ( 1 (
·𝑠 ‘𝑀)𝑣) = ( 1 (
·𝑠 ‘𝑀)𝑍)) |
| 41 | 40 | adantl 481 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) ∧ 𝑣 = 𝑍) → ( 1 (
·𝑠 ‘𝑀)𝑣) = ( 1 (
·𝑠 ‘𝑀)𝑍)) |
| 42 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 43 | 2, 42, 6 | lmod1cl 20887 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 1 ∈
(Base‘𝑆)) |
| 44 | 43 | ancli 548 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod → (𝑀 ∈ LMod ∧ 1 ∈
(Base‘𝑆))) |
| 45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 ∈ LMod ∧ 1 ∈ (Base‘𝑆))) |
| 46 | 45 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) ∧ 𝑣 = 𝑍) → (𝑀 ∈ LMod ∧ 1 ∈ (Base‘𝑆))) |
| 47 | | eqid 2737 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
| 48 | | linc0scn0.z |
. . . . . . . . 9
⊢ 𝑍 = (0g‘𝑀) |
| 49 | 2, 47, 42, 48 | lmodvs0 20894 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ 1 ∈
(Base‘𝑆)) → (
1 (
·𝑠 ‘𝑀)𝑍) = 𝑍) |
| 50 | 46, 49 | syl 17 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) ∧ 𝑣 = 𝑍) → ( 1 (
·𝑠 ‘𝑀)𝑍) = 𝑍) |
| 51 | 41, 50 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) ∧ 𝑣 = 𝑍) → ( 1 (
·𝑠 ‘𝑀)𝑣) = 𝑍) |
| 52 | 1 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) |
| 53 | | elelpwi 4610 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑣 ∈ 𝐵) |
| 54 | 53 | expcom 413 |
. . . . . . . . . 10
⊢ (𝑉 ∈ 𝒫 𝐵 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
| 55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
| 56 | 55 | imp 406 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝐵) |
| 57 | 22, 2, 47, 8, 48 | lmod0vs 20893 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) |
| 58 | 52, 56, 57 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) |
| 59 | 58 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) ∧ ¬ 𝑣 = 𝑍) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) |
| 60 | 51, 59 | ifeqda 4562 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → if(𝑣 = 𝑍, ( 1 (
·𝑠 ‘𝑀)𝑣), ( 0 (
·𝑠 ‘𝑀)𝑣)) = 𝑍) |
| 61 | 37, 39, 60 | 3eqtrd 2781 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = 𝑍) |
| 62 | 61 | mpteq2dva 5242 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ 𝑍)) |
| 63 | 62 | oveq2d 7447 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍))) |
| 64 | | lmodgrp 20865 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) |
| 65 | 64 | grpmndd 18964 |
. . 3
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd) |
| 66 | 48 | gsumz 18849 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍)) = 𝑍) |
| 67 | 65, 66 | sylan 580 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍)) = 𝑍) |
| 68 | 28, 63, 67 | 3eqtrd 2781 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) |