Proof of Theorem lincresunit3lem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl2 1192 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝑀 ∈ LMod) | 
| 2 |  | lincresunit.e | . . . . . . . . . 10
⊢ 𝐸 = (Base‘𝑅) | 
| 3 |  | lincresunit.r | . . . . . . . . . . 11
⊢ 𝑅 = (Scalar‘𝑀) | 
| 4 | 3 | fveq2i 6908 | . . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘(Scalar‘𝑀)) | 
| 5 | 2, 4 | eqtri 2764 | . . . . . . . . 9
⊢ 𝐸 =
(Base‘(Scalar‘𝑀)) | 
| 6 | 5 | oveq1i 7442 | . . . . . . . 8
⊢ (𝐸 ↑m 𝑆) =
((Base‘(Scalar‘𝑀)) ↑m 𝑆) | 
| 7 | 6 | eleq2i 2832 | . . . . . . 7
⊢ (𝐹 ∈ (𝐸 ↑m 𝑆) ↔ 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆)) | 
| 8 | 7 | biimpi 216 | . . . . . 6
⊢ (𝐹 ∈ (𝐸 ↑m 𝑆) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆)) | 
| 9 | 8 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆)) | 
| 10 | 9 | adantl 481 | . . . 4
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑆)) | 
| 11 |  | difssd 4136 | . . . 4
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑆 ∖ {𝑋}) ⊆ 𝑆) | 
| 12 |  | elmapssres 8908 | . . . 4
⊢ ((𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑆) ∧ (𝑆 ∖ {𝑋}) ⊆ 𝑆) → (𝐹 ↾ (𝑆 ∖ {𝑋})) ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑋}))) | 
| 13 | 10, 11, 12 | syl2anc 584 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝐹 ↾ (𝑆 ∖ {𝑋})) ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑋}))) | 
| 14 |  | elpwi 4606 | . . . . . . . 8
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) → 𝑆 ⊆ (Base‘𝑀)) | 
| 15 | 14 | ssdifssd 4146 | . . . . . . 7
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑋}) ⊆ (Base‘𝑀)) | 
| 16 |  | difexg 5328 | . . . . . . . 8
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑋}) ∈ V) | 
| 17 |  | elpwg 4602 | . . . . . . . 8
⊢ ((𝑆 ∖ {𝑋}) ∈ V → ((𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑋}) ⊆ (Base‘𝑀))) | 
| 18 | 16, 17 | syl 17 | . . . . . . 7
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
((𝑆 ∖ {𝑋}) ∈ 𝒫
(Base‘𝑀) ↔
(𝑆 ∖ {𝑋}) ⊆ (Base‘𝑀))) | 
| 19 | 15, 18 | mpbird 257 | . . . . . 6
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑋}) ∈ 𝒫
(Base‘𝑀)) | 
| 20 |  | lincresunit.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑀) | 
| 21 | 20 | pweqi 4615 | . . . . . 6
⊢ 𝒫
𝐵 = 𝒫
(Base‘𝑀) | 
| 22 | 19, 21 | eleq2s 2858 | . . . . 5
⊢ (𝑆 ∈ 𝒫 𝐵 → (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) | 
| 23 | 22 | 3ad2ant1 1133 | . . . 4
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) | 
| 24 | 23 | adantr 480 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) | 
| 25 |  | lincval 48331 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝐹 ↾ (𝑆 ∖ {𝑋})) ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑋})) ∧ (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) → ((𝐹 ↾ (𝑆 ∖ {𝑋}))( linC ‘𝑀)(𝑆 ∖ {𝑋})) = (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ (((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)( ·𝑠
‘𝑀)𝑧)))) | 
| 26 | 1, 13, 24, 25 | syl3anc 1372 | . 2
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → ((𝐹 ↾ (𝑆 ∖ {𝑋}))( linC ‘𝑀)(𝑆 ∖ {𝑋})) = (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ (((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)( ·𝑠
‘𝑀)𝑧)))) | 
| 27 |  | simpll 766 | . . . . . 6
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆)) | 
| 28 |  | simplr1 1215 | . . . . . 6
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → 𝐹 ∈ (𝐸 ↑m 𝑆)) | 
| 29 |  | simplr2 1216 | . . . . . 6
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → (𝐹‘𝑋) ∈ 𝑈) | 
| 30 |  | simpr 484 | . . . . . 6
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → 𝑧 ∈ (𝑆 ∖ {𝑋})) | 
| 31 |  | lincresunit.u | . . . . . . 7
⊢ 𝑈 = (Unit‘𝑅) | 
| 32 |  | lincresunit.0 | . . . . . . 7
⊢  0 =
(0g‘𝑅) | 
| 33 |  | lincresunit.z | . . . . . . 7
⊢ 𝑍 = (0g‘𝑀) | 
| 34 |  | lincresunit.n | . . . . . . 7
⊢ 𝑁 = (invg‘𝑅) | 
| 35 |  | lincresunit.i | . . . . . . 7
⊢ 𝐼 = (invr‘𝑅) | 
| 36 |  | lincresunit.t | . . . . . . 7
⊢  · =
(.r‘𝑅) | 
| 37 |  | lincresunit.g | . . . . . . 7
⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) | 
| 38 | 20, 3, 2, 31, 32, 33, 34, 35, 36, 37 | lincresunit3lem1 48401 | . . . . . 6
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋}))) → ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠
‘𝑀)𝑧)) | 
| 39 | 27, 28, 29, 30, 38 | syl13anc 1373 | . . . . 5
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠
‘𝑀)𝑧)) | 
| 40 |  | fvres 6924 | . . . . . . . 8
⊢ (𝑧 ∈ (𝑆 ∖ {𝑋}) → ((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧) = (𝐹‘𝑧)) | 
| 41 | 40 | adantl 481 | . . . . . . 7
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → ((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧) = (𝐹‘𝑧)) | 
| 42 | 41 | eqcomd 2742 | . . . . . 6
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → (𝐹‘𝑧) = ((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)) | 
| 43 | 42 | oveq1d 7447 | . . . . 5
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → ((𝐹‘𝑧)( ·𝑠
‘𝑀)𝑧) = (((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)( ·𝑠
‘𝑀)𝑧)) | 
| 44 | 39, 43 | eqtrd 2776 | . . . 4
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)) = (((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)( ·𝑠
‘𝑀)𝑧)) | 
| 45 | 44 | mpteq2dva 5241 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧))) = (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ (((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)( ·𝑠
‘𝑀)𝑧))) | 
| 46 | 45 | oveq2d 7448 | . 2
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑀 Σg
(𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)))) = (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ (((𝐹 ↾ (𝑆 ∖ {𝑋}))‘𝑧)( ·𝑠
‘𝑀)𝑧)))) | 
| 47 |  | eqid 2736 | . . 3
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 48 |  | eqid 2736 | . . 3
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) | 
| 49 |  | difexg 5328 | . . . . 5
⊢ (𝑆 ∈ 𝒫 𝐵 → (𝑆 ∖ {𝑋}) ∈ V) | 
| 50 | 49 | 3ad2ant1 1133 | . . . 4
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑆 ∖ {𝑋}) ∈ V) | 
| 51 | 50 | adantr 480 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑆 ∖ {𝑋}) ∈ V) | 
| 52 | 3 | lmodfgrp 20868 | . . . . . . 7
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Grp) | 
| 53 | 52 | 3ad2ant2 1134 | . . . . . 6
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → 𝑅 ∈ Grp) | 
| 54 | 53 | adantr 480 | . . . . 5
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ 𝐹 ∈ (𝐸 ↑m 𝑆)) → 𝑅 ∈ Grp) | 
| 55 |  | elmapi 8890 | . . . . . . 7
⊢ (𝐹 ∈ (𝐸 ↑m 𝑆) → 𝐹:𝑆⟶𝐸) | 
| 56 |  | ffvelcdm 7100 | . . . . . . . . 9
⊢ ((𝐹:𝑆⟶𝐸 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ 𝐸) | 
| 57 | 56 | expcom 413 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑆 → (𝐹:𝑆⟶𝐸 → (𝐹‘𝑋) ∈ 𝐸)) | 
| 58 | 57 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝐹:𝑆⟶𝐸 → (𝐹‘𝑋) ∈ 𝐸)) | 
| 59 | 55, 58 | syl5com 31 | . . . . . 6
⊢ (𝐹 ∈ (𝐸 ↑m 𝑆) → ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ 𝐸)) | 
| 60 | 59 | impcom 407 | . . . . 5
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ 𝐹 ∈ (𝐸 ↑m 𝑆)) → (𝐹‘𝑋) ∈ 𝐸) | 
| 61 | 2, 34 | grpinvcl 19006 | . . . . 5
⊢ ((𝑅 ∈ Grp ∧ (𝐹‘𝑋) ∈ 𝐸) → (𝑁‘(𝐹‘𝑋)) ∈ 𝐸) | 
| 62 | 54, 60, 61 | syl2anc 584 | . . . 4
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ 𝐹 ∈ (𝐸 ↑m 𝑆)) → (𝑁‘(𝐹‘𝑋)) ∈ 𝐸) | 
| 63 | 62 | 3ad2antr1 1188 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑁‘(𝐹‘𝑋)) ∈ 𝐸) | 
| 64 | 1 | adantr 480 | . . . 4
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → 𝑀 ∈ LMod) | 
| 65 | 20, 3, 2, 31, 32, 33, 34, 35, 36, 37 | lincresunit1 48399 | . . . . . . 7
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) | 
| 66 | 65 | 3adantr3 1171 | . . . . . 6
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) | 
| 67 |  | elmapi 8890 | . . . . . 6
⊢ (𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})) → 𝐺:(𝑆 ∖ {𝑋})⟶𝐸) | 
| 68 |  | ffvelcdm 7100 | . . . . . . 7
⊢ ((𝐺:(𝑆 ∖ {𝑋})⟶𝐸 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → (𝐺‘𝑧) ∈ 𝐸) | 
| 69 | 68 | ex 412 | . . . . . 6
⊢ (𝐺:(𝑆 ∖ {𝑋})⟶𝐸 → (𝑧 ∈ (𝑆 ∖ {𝑋}) → (𝐺‘𝑧) ∈ 𝐸)) | 
| 70 | 66, 67, 69 | 3syl 18 | . . . . 5
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑋}) → (𝐺‘𝑧) ∈ 𝐸)) | 
| 71 | 70 | imp 406 | . . . 4
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → (𝐺‘𝑧) ∈ 𝐸) | 
| 72 |  | elpwi 4606 | . . . . . . . 8
⊢ (𝑆 ∈ 𝒫 𝐵 → 𝑆 ⊆ 𝐵) | 
| 73 |  | eldifi 4130 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝑆 ∖ {𝑋}) → 𝑧 ∈ 𝑆) | 
| 74 |  | ssel2 3977 | . . . . . . . . . 10
⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵) | 
| 75 | 74 | expcom 413 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝑆 → (𝑆 ⊆ 𝐵 → 𝑧 ∈ 𝐵)) | 
| 76 | 73, 75 | syl 17 | . . . . . . . 8
⊢ (𝑧 ∈ (𝑆 ∖ {𝑋}) → (𝑆 ⊆ 𝐵 → 𝑧 ∈ 𝐵)) | 
| 77 | 72, 76 | syl5com 31 | . . . . . . 7
⊢ (𝑆 ∈ 𝒫 𝐵 → (𝑧 ∈ (𝑆 ∖ {𝑋}) → 𝑧 ∈ 𝐵)) | 
| 78 | 77 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑧 ∈ (𝑆 ∖ {𝑋}) → 𝑧 ∈ 𝐵)) | 
| 79 | 78 | adantr 480 | . . . . 5
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑋}) → 𝑧 ∈ 𝐵)) | 
| 80 | 79 | imp 406 | . . . 4
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → 𝑧 ∈ 𝐵) | 
| 81 | 20, 3, 48, 2 | lmodvscl 20877 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐺‘𝑧) ∈ 𝐸 ∧ 𝑧 ∈ 𝐵) → ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧) ∈ 𝐵) | 
| 82 | 64, 71, 80, 81 | syl3anc 1372 | . . 3
⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) ∧ 𝑧 ∈ (𝑆 ∖ {𝑋})) → ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧) ∈ 𝐵) | 
| 83 |  | simp2 1137 | . . . . . 6
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → 𝑀 ∈ LMod) | 
| 84 | 83, 23 | jca 511 | . . . . 5
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀))) | 
| 85 | 84 | adantr 480 | . . . 4
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀))) | 
| 86 | 20, 3, 2, 31, 32, 33, 34, 35, 36, 37 | lincresunit2 48400 | . . . . 5
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐺 finSupp 0 ) | 
| 87 | 86, 32 | breqtrdi 5183 | . . . 4
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐺 finSupp
(0g‘𝑅)) | 
| 88 | 3, 2 | scmfsupp 48296 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})) ∧ 𝐺 finSupp (0g‘𝑅)) → (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)) finSupp (0g‘𝑀)) | 
| 89 | 88, 33 | breqtrrdi 5184 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})) ∧ 𝐺 finSupp (0g‘𝑅)) → (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)) finSupp 𝑍) | 
| 90 | 85, 66, 87, 89 | syl3anc 1372 | . . 3
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)) finSupp 𝑍) | 
| 91 | 20, 3, 2, 33, 47, 48, 1, 51, 63, 82, 90 | gsumvsmul 20925 | . 2
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → (𝑀 Σg
(𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)))) = ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)(𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧))))) | 
| 92 | 26, 46, 91 | 3eqtr2rd 2783 | 1
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → ((𝑁‘(𝐹‘𝑋))( ·𝑠
‘𝑀)(𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠
‘𝑀)𝑧)))) = ((𝐹 ↾ (𝑆 ∖ {𝑋}))( linC ‘𝑀)(𝑆 ∖ {𝑋}))) |