MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmsslsp Structured version   Visualization version   GIF version

Theorem frlmsslsp 21734
Description: A subset of a free module obtained by restricting the support set is spanned by the relevant unit vectors. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by AV, 24-Jun-2019.)
Hypotheses
Ref Expression
frlmsslsp.y π‘Œ = (𝑅 freeLMod 𝐼)
frlmsslsp.u π‘ˆ = (𝑅 unitVec 𝐼)
frlmsslsp.k 𝐾 = (LSpanβ€˜π‘Œ)
frlmsslsp.b 𝐡 = (Baseβ€˜π‘Œ)
frlmsslsp.z 0 = (0gβ€˜π‘…)
frlmsslsp.c 𝐢 = {π‘₯ ∈ 𝐡 ∣ (π‘₯ supp 0 ) βŠ† 𝐽}
Assertion
Ref Expression
frlmsslsp ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) = 𝐢)
Distinct variable groups:   π‘₯,π‘Œ   π‘₯,π‘ˆ   π‘₯,𝐡   π‘₯, 0   π‘₯,𝑅   π‘₯,𝐼   π‘₯,𝑉   π‘₯,𝐽   π‘₯,𝐾
Allowed substitution hint:   𝐢(π‘₯)

Proof of Theorem frlmsslsp
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frlmsslsp.y . . . . 5 π‘Œ = (𝑅 freeLMod 𝐼)
21frlmlmod 21687 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) β†’ π‘Œ ∈ LMod)
323adant3 1129 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘Œ ∈ LMod)
4 eqid 2725 . . . 4 (LSubSpβ€˜π‘Œ) = (LSubSpβ€˜π‘Œ)
5 frlmsslsp.b . . . 4 𝐡 = (Baseβ€˜π‘Œ)
6 frlmsslsp.z . . . 4 0 = (0gβ€˜π‘…)
7 frlmsslsp.c . . . 4 𝐢 = {π‘₯ ∈ 𝐡 ∣ (π‘₯ supp 0 ) βŠ† 𝐽}
81, 4, 5, 6, 7frlmsslss2 21713 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐢 ∈ (LSubSpβ€˜π‘Œ))
9 frlmsslsp.u . . . . . . . . . 10 π‘ˆ = (𝑅 unitVec 𝐼)
109, 1, 5uvcff 21729 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) β†’ π‘ˆ:𝐼⟢𝐡)
11103adant3 1129 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘ˆ:𝐼⟢𝐡)
1211adantr 479 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ π‘ˆ:𝐼⟢𝐡)
13 simp3 1135 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐽 βŠ† 𝐼)
1413sselda 3972 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ 𝑦 ∈ 𝐼)
1512, 14ffvelcdmd 7090 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘¦) ∈ 𝐡)
16 simpl2 1189 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ 𝐼 ∈ 𝑉)
17 eqid 2725 . . . . . . . . 9 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
181, 17, 5frlmbasf 21698 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ (π‘ˆβ€˜π‘¦) ∈ 𝐡) β†’ (π‘ˆβ€˜π‘¦):𝐼⟢(Baseβ€˜π‘…))
1916, 15, 18syl2anc 582 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘¦):𝐼⟢(Baseβ€˜π‘…))
20 simpll1 1209 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑅 ∈ Ring)
21 simpll2 1210 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝐼 ∈ 𝑉)
2214adantr 479 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑦 ∈ 𝐼)
23 eldifi 4119 . . . . . . . . 9 (π‘₯ ∈ (𝐼 βˆ– 𝐽) β†’ π‘₯ ∈ 𝐼)
2423adantl 480 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ π‘₯ ∈ 𝐼)
25 elneeldif 3953 . . . . . . . . 9 ((𝑦 ∈ 𝐽 ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑦 β‰  π‘₯)
2625adantll 712 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑦 β‰  π‘₯)
279, 20, 21, 22, 24, 26, 6uvcvv0 21728 . . . . . . 7 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ ((π‘ˆβ€˜π‘¦)β€˜π‘₯) = 0 )
2819, 27suppss 8197 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ ((π‘ˆβ€˜π‘¦) supp 0 ) βŠ† 𝐽)
29 oveq1 7423 . . . . . . . 8 (π‘₯ = (π‘ˆβ€˜π‘¦) β†’ (π‘₯ supp 0 ) = ((π‘ˆβ€˜π‘¦) supp 0 ))
3029sseq1d 4004 . . . . . . 7 (π‘₯ = (π‘ˆβ€˜π‘¦) β†’ ((π‘₯ supp 0 ) βŠ† 𝐽 ↔ ((π‘ˆβ€˜π‘¦) supp 0 ) βŠ† 𝐽))
3130, 7elrab2 3677 . . . . . 6 ((π‘ˆβ€˜π‘¦) ∈ 𝐢 ↔ ((π‘ˆβ€˜π‘¦) ∈ 𝐡 ∧ ((π‘ˆβ€˜π‘¦) supp 0 ) βŠ† 𝐽))
3215, 28, 31sylanbrc 581 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘¦) ∈ 𝐢)
3332ralrimiva 3136 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘ˆβ€˜π‘¦) ∈ 𝐢)
3411ffund 6721 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ Fun π‘ˆ)
3511fdmd 6728 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ dom π‘ˆ = 𝐼)
3613, 35sseqtrrd 4014 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐽 βŠ† dom π‘ˆ)
37 funimass4 6958 . . . . 5 ((Fun π‘ˆ ∧ 𝐽 βŠ† dom π‘ˆ) β†’ ((π‘ˆ β€œ 𝐽) βŠ† 𝐢 ↔ βˆ€π‘¦ ∈ 𝐽 (π‘ˆβ€˜π‘¦) ∈ 𝐢))
3834, 36, 37syl2anc 582 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ ((π‘ˆ β€œ 𝐽) βŠ† 𝐢 ↔ βˆ€π‘¦ ∈ 𝐽 (π‘ˆβ€˜π‘¦) ∈ 𝐢))
3933, 38mpbird 256 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (π‘ˆ β€œ 𝐽) βŠ† 𝐢)
40 frlmsslsp.k . . . 4 𝐾 = (LSpanβ€˜π‘Œ)
414, 40lspssp 20876 . . 3 ((π‘Œ ∈ LMod ∧ 𝐢 ∈ (LSubSpβ€˜π‘Œ) ∧ (π‘ˆ β€œ 𝐽) βŠ† 𝐢) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) βŠ† 𝐢)
423, 8, 39, 41syl3anc 1368 . 2 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) βŠ† 𝐢)
43 simpl1 1188 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑅 ∈ Ring)
44 simpl2 1189 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝐼 ∈ 𝑉)
457ssrab3 4072 . . . . . 6 𝐢 βŠ† 𝐡
4645a1i 11 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐢 βŠ† 𝐡)
4746sselda 3972 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐡)
48 eqid 2725 . . . . 5 ( ·𝑠 β€˜π‘Œ) = ( ·𝑠 β€˜π‘Œ)
499, 1, 5, 48uvcresum 21731 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 = (π‘Œ Ξ£g (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)))
5043, 44, 47, 49syl3anc 1368 . . 3 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 = (π‘Œ Ξ£g (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)))
51 eqid 2725 . . . 4 (0gβ€˜π‘Œ) = (0gβ€˜π‘Œ)
52 lmodabl 20796 . . . . . 6 (π‘Œ ∈ LMod β†’ π‘Œ ∈ Abel)
533, 52syl 17 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘Œ ∈ Abel)
5453adantr 479 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ π‘Œ ∈ Abel)
55 imassrn 6069 . . . . . . . 8 (π‘ˆ β€œ 𝐽) βŠ† ran π‘ˆ
5611frnd 6725 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ ran π‘ˆ βŠ† 𝐡)
5755, 56sstrid 3984 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (π‘ˆ β€œ 𝐽) βŠ† 𝐡)
585, 4, 40lspcl 20864 . . . . . . 7 ((π‘Œ ∈ LMod ∧ (π‘ˆ β€œ 𝐽) βŠ† 𝐡) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
593, 57, 58syl2anc 582 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
604lsssubg 20845 . . . . . 6 ((π‘Œ ∈ LMod ∧ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ)) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (SubGrpβ€˜π‘Œ))
613, 59, 60syl2anc 582 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (SubGrpβ€˜π‘Œ))
6261adantr 479 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (SubGrpβ€˜π‘Œ))
631, 17, 5frlmbasf 21698 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
64633ad2antl2 1183 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
6564ffnd 6718 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 Fn 𝐼)
6611ffnd 6718 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘ˆ Fn 𝐼)
6766adantr 479 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ π‘ˆ Fn 𝐼)
68 simpl2 1189 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 𝐼 ∈ 𝑉)
69 inidm 4213 . . . . . . 7 (𝐼 ∩ 𝐼) = 𝐼
7065, 67, 68, 68, 69offn 7695 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼)
7147, 70syldan 589 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼)
7247, 65syldan 589 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 Fn 𝐼)
7372adantrr 715 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ 𝑦 Fn 𝐼)
7466adantr 479 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ π‘ˆ Fn 𝐼)
75 simpl2 1189 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ 𝐼 ∈ 𝑉)
76 simprr 771 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ 𝑧 ∈ 𝐼)
77 fnfvof 7699 . . . . . . . . 9 (((𝑦 Fn 𝐼 ∧ π‘ˆ Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) = ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)))
7873, 74, 75, 76, 77syl22anc 837 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) = ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)))
793adantr 479 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ π‘Œ ∈ LMod)
8059adantr 479 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
8145sseli 3968 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝐢 β†’ 𝑦 ∈ 𝐡)
8281, 64sylan2 591 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
8382adantrr 715 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
8413sselda 3972 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑧 ∈ 𝐽) β†’ 𝑧 ∈ 𝐼)
8584adantrl 714 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ 𝑧 ∈ 𝐼)
8683, 85ffvelcdmd 7090 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘¦β€˜π‘§) ∈ (Baseβ€˜π‘…))
871frlmsca 21691 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) β†’ 𝑅 = (Scalarβ€˜π‘Œ))
88873adant3 1129 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝑅 = (Scalarβ€˜π‘Œ))
8988fveq2d 6896 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘Œ)))
9089adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘Œ)))
9186, 90eleqtrd 2827 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘¦β€˜π‘§) ∈ (Baseβ€˜(Scalarβ€˜π‘Œ)))
925, 40lspssid 20873 . . . . . . . . . . . . . . 15 ((π‘Œ ∈ LMod ∧ (π‘ˆ β€œ 𝐽) βŠ† 𝐡) β†’ (π‘ˆ β€œ 𝐽) βŠ† (πΎβ€˜(π‘ˆ β€œ 𝐽)))
933, 57, 92syl2anc 582 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (π‘ˆ β€œ 𝐽) βŠ† (πΎβ€˜(π‘ˆ β€œ 𝐽)))
9493adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘ˆ β€œ 𝐽) βŠ† (πΎβ€˜(π‘ˆ β€œ 𝐽)))
95 funfvima2 7239 . . . . . . . . . . . . . . . 16 ((Fun π‘ˆ ∧ 𝐽 βŠ† dom π‘ˆ) β†’ (𝑧 ∈ 𝐽 β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽)))
9634, 36, 95syl2anc 582 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (𝑧 ∈ 𝐽 β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽)))
9796imp 405 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑧 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽))
9897adantrl 714 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽))
9994, 98sseldd 3973 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘ˆβ€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
100 eqid 2725 . . . . . . . . . . . . 13 (Scalarβ€˜π‘Œ) = (Scalarβ€˜π‘Œ)
101 eqid 2725 . . . . . . . . . . . . 13 (Baseβ€˜(Scalarβ€˜π‘Œ)) = (Baseβ€˜(Scalarβ€˜π‘Œ))
102100, 48, 101, 4lssvscl 20843 . . . . . . . . . . . 12 (((π‘Œ ∈ LMod ∧ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ)) ∧ ((π‘¦β€˜π‘§) ∈ (Baseβ€˜(Scalarβ€˜π‘Œ)) ∧ (π‘ˆβ€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
10379, 80, 91, 99, 102syl22anc 837 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
104103anassrs 466 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) ∧ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
105104adantlrr 719 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
106 id 22 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢))
107106adantrr 715 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢))
108107adantr 479 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢))
109 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ 𝑧 ∈ 𝐼)
110 simpr 483 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ Β¬ 𝑧 ∈ 𝐽)
111109, 110eldifd 3950 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ 𝑧 ∈ (𝐼 βˆ– 𝐽))
112 oveq1 7423 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑦 β†’ (π‘₯ supp 0 ) = (𝑦 supp 0 ))
113112sseq1d 4004 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ ((π‘₯ supp 0 ) βŠ† 𝐽 ↔ (𝑦 supp 0 ) βŠ† 𝐽))
114113, 7elrab2 3677 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝐢 ↔ (𝑦 ∈ 𝐡 ∧ (𝑦 supp 0 ) βŠ† 𝐽))
115114simprbi 495 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝐢 β†’ (𝑦 supp 0 ) βŠ† 𝐽)
116115adantl 480 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 supp 0 ) βŠ† 𝐽)
1176fvexi 6906 . . . . . . . . . . . . . . . 16 0 ∈ V
118117a1i 11 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 0 ∈ V)
11982, 116, 44, 118suppssr 8199 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) ∧ 𝑧 ∈ (𝐼 βˆ– 𝐽)) β†’ (π‘¦β€˜π‘§) = 0 )
120108, 111, 119syl2anc 582 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (π‘¦β€˜π‘§) = 0 )
12188fveq2d 6896 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘Œ)))
1226, 121eqtrid 2777 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 0 = (0gβ€˜(Scalarβ€˜π‘Œ)))
123122ad2antrr 724 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ 0 = (0gβ€˜(Scalarβ€˜π‘Œ)))
124120, 123eqtrd 2765 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (π‘¦β€˜π‘§) = (0gβ€˜(Scalarβ€˜π‘Œ)))
125124oveq1d 7431 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)))
1263ad2antrr 724 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ π‘Œ ∈ LMod)
12711ffvelcdmda 7089 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑧 ∈ 𝐼) β†’ (π‘ˆβ€˜π‘§) ∈ 𝐡)
128127adantrl 714 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ (π‘ˆβ€˜π‘§) ∈ 𝐡)
129128adantr 479 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘§) ∈ 𝐡)
130 eqid 2725 . . . . . . . . . . . . 13 (0gβ€˜(Scalarβ€˜π‘Œ)) = (0gβ€˜(Scalarβ€˜π‘Œ))
1315, 100, 48, 130, 51lmod0vs 20782 . . . . . . . . . . . 12 ((π‘Œ ∈ LMod ∧ (π‘ˆβ€˜π‘§) ∈ 𝐡) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = (0gβ€˜π‘Œ))
132126, 129, 131syl2anc 582 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = (0gβ€˜π‘Œ))
133125, 132eqtrd 2765 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = (0gβ€˜π‘Œ))
13459ad2antrr 724 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
13551, 4lss0cl 20835 . . . . . . . . . . 11 ((π‘Œ ∈ LMod ∧ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ)) β†’ (0gβ€˜π‘Œ) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
136126, 134, 135syl2anc 582 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (0gβ€˜π‘Œ) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
137133, 136eqeltrd 2825 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
138105, 137pm2.61dan 811 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
13978, 138eqeltrd 2825 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
140139expr 455 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑧 ∈ 𝐼 β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽))))
141140ralrimiv 3135 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ βˆ€π‘§ ∈ 𝐼 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
142 ffnfv 7124 . . . . 5 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢(πΎβ€˜(π‘ˆ β€œ 𝐽)) ↔ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼 ∧ βˆ€π‘§ ∈ 𝐼 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽))))
14371, 141, 142sylanbrc 581 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢(πΎβ€˜(π‘ˆ β€œ 𝐽)))
1441, 6, 5frlmbasfsupp 21696 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 finSupp 0 )
145144fsuppimpd 9393 . . . . . . 7 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 supp 0 ) ∈ Fin)
14644, 47, 145syl2anc 582 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 supp 0 ) ∈ Fin)
147 dffn2 6719 . . . . . . . . 9 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼 ↔ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢V)
14870, 147sylib 217 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢V)
14965adantr 479 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ 𝑦 Fn 𝐼)
15066ad2antrr 724 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ π‘ˆ Fn 𝐼)
151 simpll2 1210 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ 𝐼 ∈ 𝑉)
152 eldifi 4119 . . . . . . . . . . 11 (π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 )) β†’ π‘₯ ∈ 𝐼)
153152adantl 480 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ π‘₯ ∈ 𝐼)
154 fnfvof 7699 . . . . . . . . . 10 (((𝑦 Fn 𝐼 ∧ π‘ˆ Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘₯) = ((π‘¦β€˜π‘₯)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)))
155149, 150, 151, 153, 154syl22anc 837 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘₯) = ((π‘¦β€˜π‘₯)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)))
156 ssidd 3996 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 supp 0 ) βŠ† (𝑦 supp 0 ))
157117a1i 11 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 0 ∈ V)
15864, 156, 68, 157suppssr 8199 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ (π‘¦β€˜π‘₯) = 0 )
159122ad2antrr 724 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ 0 = (0gβ€˜(Scalarβ€˜π‘Œ)))
160158, 159eqtrd 2765 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ (π‘¦β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘Œ)))
161160oveq1d 7431 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((π‘¦β€˜π‘₯)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)) = ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)))
1623ad2antrr 724 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ π‘Œ ∈ LMod)
16311adantr 479 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ π‘ˆ:𝐼⟢𝐡)
164 ffvelcdm 7086 . . . . . . . . . . 11 ((π‘ˆ:𝐼⟢𝐡 ∧ π‘₯ ∈ 𝐼) β†’ (π‘ˆβ€˜π‘₯) ∈ 𝐡)
165163, 152, 164syl2an 594 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ (π‘ˆβ€˜π‘₯) ∈ 𝐡)
1665, 100, 48, 130, 51lmod0vs 20782 . . . . . . . . . 10 ((π‘Œ ∈ LMod ∧ (π‘ˆβ€˜π‘₯) ∈ 𝐡) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)) = (0gβ€˜π‘Œ))
167162, 165, 166syl2anc 582 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)) = (0gβ€˜π‘Œ))
168155, 161, 1673eqtrd 2769 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘₯) = (0gβ€˜π‘Œ))
169148, 168suppss 8197 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) βŠ† (𝑦 supp 0 ))
17047, 169syldan 589 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) βŠ† (𝑦 supp 0 ))
171146, 170ssfid 9290 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) ∈ Fin)
172 simp2 1134 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐼 ∈ 𝑉)
1731, 17, 5frlmbasmap 21697 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m 𝐼))
174172, 81, 173syl2an 594 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m 𝐼))
175 elmapfn 8882 . . . . . . . 8 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) β†’ 𝑦 Fn 𝐼)
176174, 175syl 17 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 Fn 𝐼)
17711adantr 479 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ π‘ˆ:𝐼⟢𝐡)
178177ffnd 6718 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ π‘ˆ Fn 𝐼)
179176, 178, 44, 44offun 7696 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ Fun (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ))
180 ovexd 7451 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) ∈ V)
181 fvexd 6907 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (0gβ€˜π‘Œ) ∈ V)
182 funisfsupp 9391 . . . . . 6 ((Fun (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) ∧ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) ∈ V ∧ (0gβ€˜π‘Œ) ∈ V) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) finSupp (0gβ€˜π‘Œ) ↔ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) ∈ Fin))
183179, 180, 181, 182syl3anc 1368 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) finSupp (0gβ€˜π‘Œ) ↔ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) ∈ Fin))
184171, 183mpbird 256 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) finSupp (0gβ€˜π‘Œ))
18551, 54, 44, 62, 143, 184gsumsubgcl 19879 . . 3 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (π‘Œ Ξ£g (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
18650, 185eqeltrd 2825 . 2 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
18742, 186eqelssd 3994 1 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) = 𝐢)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  {crab 3419  Vcvv 3463   βˆ– cdif 3936   βŠ† wss 3939   class class class wbr 5143  dom cdm 5672  ran crn 5673   β€œ cima 5675  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7416   ∘f cof 7680   supp csupp 8163   ↑m cmap 8843  Fincfn 8962   finSupp cfsupp 9385  Basecbs 17179  Scalarcsca 17235   ·𝑠 cvsca 17236  0gc0g 17420   Ξ£g cgsu 17421  SubGrpcsubg 19079  Abelcabl 19740  Ringcrg 20177  LModclmod 20747  LSubSpclss 20819  LSpanclspn 20859   freeLMod cfrlm 21684   unitVec cuvc 21720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7991  df-2nd 7992  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-map 8845  df-ixp 8915  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-fsupp 9386  df-sup 9465  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312  df-n0 12503  df-z 12589  df-dec 12708  df-uz 12853  df-fz 13517  df-fzo 13660  df-seq 13999  df-hash 14322  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-mulr 17246  df-sca 17248  df-vsca 17249  df-ip 17250  df-tset 17251  df-ple 17252  df-ds 17254  df-hom 17256  df-cco 17257  df-0g 17422  df-gsum 17423  df-prds 17428  df-pws 17430  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18739  df-submnd 18740  df-grp 18897  df-minusg 18898  df-sbg 18899  df-mulg 19028  df-subg 19082  df-ghm 19172  df-cntz 19272  df-cmn 19741  df-abl 19742  df-mgp 20079  df-rng 20097  df-ur 20126  df-ring 20179  df-subrg 20512  df-lmod 20749  df-lss 20820  df-lsp 20860  df-lmhm 20911  df-sra 21062  df-rgmod 21063  df-dsmm 21670  df-frlm 21685  df-uvc 21721
This theorem is referenced by:  frlmlbs  21735
  Copyright terms: Public domain W3C validator