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

Theorem frlmsslsp 21691
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 21644 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) β†’ π‘Œ ∈ LMod)
323adant3 1129 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘Œ ∈ LMod)
4 eqid 2726 . . . 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 21670 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐢 ∈ (LSubSpβ€˜π‘Œ))
9 frlmsslsp.u . . . . . . . . . 10 π‘ˆ = (𝑅 unitVec 𝐼)
109, 1, 5uvcff 21686 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) β†’ π‘ˆ:𝐼⟢𝐡)
11103adant3 1129 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘ˆ:𝐼⟢𝐡)
1211adantr 480 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ π‘ˆ:𝐼⟢𝐡)
13 simp3 1135 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐽 βŠ† 𝐼)
1413sselda 3977 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ 𝑦 ∈ 𝐼)
1512, 14ffvelcdmd 7081 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘¦) ∈ 𝐡)
16 simpl2 1189 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ 𝐼 ∈ 𝑉)
17 eqid 2726 . . . . . . . . 9 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
181, 17, 5frlmbasf 21655 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ (π‘ˆβ€˜π‘¦) ∈ 𝐡) β†’ (π‘ˆβ€˜π‘¦):𝐼⟢(Baseβ€˜π‘…))
1916, 15, 18syl2anc 583 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘¦):𝐼⟢(Baseβ€˜π‘…))
20 simpll1 1209 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑅 ∈ Ring)
21 simpll2 1210 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝐼 ∈ 𝑉)
2214adantr 480 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑦 ∈ 𝐼)
23 eldifi 4121 . . . . . . . . 9 (π‘₯ ∈ (𝐼 βˆ– 𝐽) β†’ π‘₯ ∈ 𝐼)
2423adantl 481 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ π‘₯ ∈ 𝐼)
25 elneeldif 3957 . . . . . . . . 9 ((𝑦 ∈ 𝐽 ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑦 β‰  π‘₯)
2625adantll 711 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ 𝑦 β‰  π‘₯)
279, 20, 21, 22, 24, 26, 6uvcvv0 21685 . . . . . . 7 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) ∧ π‘₯ ∈ (𝐼 βˆ– 𝐽)) β†’ ((π‘ˆβ€˜π‘¦)β€˜π‘₯) = 0 )
2819, 27suppss 8179 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ ((π‘ˆβ€˜π‘¦) supp 0 ) βŠ† 𝐽)
29 oveq1 7412 . . . . . . . 8 (π‘₯ = (π‘ˆβ€˜π‘¦) β†’ (π‘₯ supp 0 ) = ((π‘ˆβ€˜π‘¦) supp 0 ))
3029sseq1d 4008 . . . . . . 7 (π‘₯ = (π‘ˆβ€˜π‘¦) β†’ ((π‘₯ supp 0 ) βŠ† 𝐽 ↔ ((π‘ˆβ€˜π‘¦) supp 0 ) βŠ† 𝐽))
3130, 7elrab2 3681 . . . . . 6 ((π‘ˆβ€˜π‘¦) ∈ 𝐢 ↔ ((π‘ˆβ€˜π‘¦) ∈ 𝐡 ∧ ((π‘ˆβ€˜π‘¦) supp 0 ) βŠ† 𝐽))
3215, 28, 31sylanbrc 582 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘¦) ∈ 𝐢)
3332ralrimiva 3140 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘ˆβ€˜π‘¦) ∈ 𝐢)
3411ffund 6715 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ Fun π‘ˆ)
3511fdmd 6722 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ dom π‘ˆ = 𝐼)
3613, 35sseqtrrd 4018 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐽 βŠ† dom π‘ˆ)
37 funimass4 6950 . . . . 5 ((Fun π‘ˆ ∧ 𝐽 βŠ† dom π‘ˆ) β†’ ((π‘ˆ β€œ 𝐽) βŠ† 𝐢 ↔ βˆ€π‘¦ ∈ 𝐽 (π‘ˆβ€˜π‘¦) ∈ 𝐢))
3834, 36, 37syl2anc 583 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ ((π‘ˆ β€œ 𝐽) βŠ† 𝐢 ↔ βˆ€π‘¦ ∈ 𝐽 (π‘ˆβ€˜π‘¦) ∈ 𝐢))
3933, 38mpbird 257 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (π‘ˆ β€œ 𝐽) βŠ† 𝐢)
40 frlmsslsp.k . . . 4 𝐾 = (LSpanβ€˜π‘Œ)
414, 40lspssp 20835 . . 3 ((π‘Œ ∈ LMod ∧ 𝐢 ∈ (LSubSpβ€˜π‘Œ) ∧ (π‘ˆ β€œ 𝐽) βŠ† 𝐢) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) βŠ† 𝐢)
423, 8, 39, 41syl3anc 1368 . 2 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) βŠ† 𝐢)
43 simpl1 1188 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑅 ∈ Ring)
44 simpl2 1189 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝐼 ∈ 𝑉)
457ssrab3 4075 . . . . . 6 𝐢 βŠ† 𝐡
4645a1i 11 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐢 βŠ† 𝐡)
4746sselda 3977 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐡)
48 eqid 2726 . . . . 5 ( ·𝑠 β€˜π‘Œ) = ( ·𝑠 β€˜π‘Œ)
499, 1, 5, 48uvcresum 21688 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 = (π‘Œ Ξ£g (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)))
5043, 44, 47, 49syl3anc 1368 . . 3 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 = (π‘Œ Ξ£g (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)))
51 eqid 2726 . . . 4 (0gβ€˜π‘Œ) = (0gβ€˜π‘Œ)
52 lmodabl 20755 . . . . . 6 (π‘Œ ∈ LMod β†’ π‘Œ ∈ Abel)
533, 52syl 17 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘Œ ∈ Abel)
5453adantr 480 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ π‘Œ ∈ Abel)
55 imassrn 6064 . . . . . . . 8 (π‘ˆ β€œ 𝐽) βŠ† ran π‘ˆ
5611frnd 6719 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ ran π‘ˆ βŠ† 𝐡)
5755, 56sstrid 3988 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (π‘ˆ β€œ 𝐽) βŠ† 𝐡)
585, 4, 40lspcl 20823 . . . . . . 7 ((π‘Œ ∈ LMod ∧ (π‘ˆ β€œ 𝐽) βŠ† 𝐡) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
593, 57, 58syl2anc 583 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
604lsssubg 20804 . . . . . 6 ((π‘Œ ∈ LMod ∧ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ)) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (SubGrpβ€˜π‘Œ))
613, 59, 60syl2anc 583 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (SubGrpβ€˜π‘Œ))
6261adantr 480 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (SubGrpβ€˜π‘Œ))
631, 17, 5frlmbasf 21655 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
64633ad2antl2 1183 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
6564ffnd 6712 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 Fn 𝐼)
6611ffnd 6712 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ π‘ˆ Fn 𝐼)
6766adantr 480 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ π‘ˆ Fn 𝐼)
68 simpl2 1189 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 𝐼 ∈ 𝑉)
69 inidm 4213 . . . . . . 7 (𝐼 ∩ 𝐼) = 𝐼
7065, 67, 68, 68, 69offn 7680 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼)
7147, 70syldan 590 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼)
7247, 65syldan 590 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 Fn 𝐼)
7372adantrr 714 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ 𝑦 Fn 𝐼)
7466adantr 480 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ π‘ˆ Fn 𝐼)
75 simpl2 1189 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ 𝐼 ∈ 𝑉)
76 simprr 770 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ 𝑧 ∈ 𝐼)
77 fnfvof 7684 . . . . . . . . 9 (((𝑦 Fn 𝐼 ∧ π‘ˆ Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) = ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)))
7873, 74, 75, 76, 77syl22anc 836 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) = ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)))
793adantr 480 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ π‘Œ ∈ LMod)
8059adantr 480 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
8145sseli 3973 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝐢 β†’ 𝑦 ∈ 𝐡)
8281, 64sylan2 592 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
8382adantrr 714 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
8413sselda 3977 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑧 ∈ 𝐽) β†’ 𝑧 ∈ 𝐼)
8584adantrl 713 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ 𝑧 ∈ 𝐼)
8683, 85ffvelcdmd 7081 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘¦β€˜π‘§) ∈ (Baseβ€˜π‘…))
871frlmsca 21648 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) β†’ 𝑅 = (Scalarβ€˜π‘Œ))
88873adant3 1129 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝑅 = (Scalarβ€˜π‘Œ))
8988fveq2d 6889 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘Œ)))
9089adantr 480 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘Œ)))
9186, 90eleqtrd 2829 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘¦β€˜π‘§) ∈ (Baseβ€˜(Scalarβ€˜π‘Œ)))
925, 40lspssid 20832 . . . . . . . . . . . . . . 15 ((π‘Œ ∈ LMod ∧ (π‘ˆ β€œ 𝐽) βŠ† 𝐡) β†’ (π‘ˆ β€œ 𝐽) βŠ† (πΎβ€˜(π‘ˆ β€œ 𝐽)))
933, 57, 92syl2anc 583 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (π‘ˆ β€œ 𝐽) βŠ† (πΎβ€˜(π‘ˆ β€œ 𝐽)))
9493adantr 480 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘ˆ β€œ 𝐽) βŠ† (πΎβ€˜(π‘ˆ β€œ 𝐽)))
95 funfvima2 7228 . . . . . . . . . . . . . . . 16 ((Fun π‘ˆ ∧ 𝐽 βŠ† dom π‘ˆ) β†’ (𝑧 ∈ 𝐽 β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽)))
9634, 36, 95syl2anc 583 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (𝑧 ∈ 𝐽 β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽)))
9796imp 406 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑧 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽))
9897adantrl 713 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘ˆβ€˜π‘§) ∈ (π‘ˆ β€œ 𝐽))
9994, 98sseldd 3978 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ (π‘ˆβ€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
100 eqid 2726 . . . . . . . . . . . . 13 (Scalarβ€˜π‘Œ) = (Scalarβ€˜π‘Œ)
101 eqid 2726 . . . . . . . . . . . . 13 (Baseβ€˜(Scalarβ€˜π‘Œ)) = (Baseβ€˜(Scalarβ€˜π‘Œ))
102100, 48, 101, 4lssvscl 20802 . . . . . . . . . . . 12 (((π‘Œ ∈ LMod ∧ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ)) ∧ ((π‘¦β€˜π‘§) ∈ (Baseβ€˜(Scalarβ€˜π‘Œ)) ∧ (π‘ˆβ€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
10379, 80, 91, 99, 102syl22anc 836 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐽)) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
104103anassrs 467 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) ∧ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
105104adantlrr 718 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
106 id 22 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢))
107106adantrr 714 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢))
108107adantr 480 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢))
109 simplrr 775 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ 𝑧 ∈ 𝐼)
110 simpr 484 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ Β¬ 𝑧 ∈ 𝐽)
111109, 110eldifd 3954 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ 𝑧 ∈ (𝐼 βˆ– 𝐽))
112 oveq1 7412 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑦 β†’ (π‘₯ supp 0 ) = (𝑦 supp 0 ))
113112sseq1d 4008 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ ((π‘₯ supp 0 ) βŠ† 𝐽 ↔ (𝑦 supp 0 ) βŠ† 𝐽))
114113, 7elrab2 3681 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝐢 ↔ (𝑦 ∈ 𝐡 ∧ (𝑦 supp 0 ) βŠ† 𝐽))
115114simprbi 496 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝐢 β†’ (𝑦 supp 0 ) βŠ† 𝐽)
116115adantl 481 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 supp 0 ) βŠ† 𝐽)
1176fvexi 6899 . . . . . . . . . . . . . . . 16 0 ∈ V
118117a1i 11 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 0 ∈ V)
11982, 116, 44, 118suppssr 8181 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) ∧ 𝑧 ∈ (𝐼 βˆ– 𝐽)) β†’ (π‘¦β€˜π‘§) = 0 )
120108, 111, 119syl2anc 583 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (π‘¦β€˜π‘§) = 0 )
12188fveq2d 6889 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘Œ)))
1226, 121eqtrid 2778 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 0 = (0gβ€˜(Scalarβ€˜π‘Œ)))
123122ad2antrr 723 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ 0 = (0gβ€˜(Scalarβ€˜π‘Œ)))
124120, 123eqtrd 2766 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (π‘¦β€˜π‘§) = (0gβ€˜(Scalarβ€˜π‘Œ)))
125124oveq1d 7420 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)))
1263ad2antrr 723 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ π‘Œ ∈ LMod)
12711ffvelcdmda 7080 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑧 ∈ 𝐼) β†’ (π‘ˆβ€˜π‘§) ∈ 𝐡)
128127adantrl 713 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ (π‘ˆβ€˜π‘§) ∈ 𝐡)
129128adantr 480 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (π‘ˆβ€˜π‘§) ∈ 𝐡)
130 eqid 2726 . . . . . . . . . . . . 13 (0gβ€˜(Scalarβ€˜π‘Œ)) = (0gβ€˜(Scalarβ€˜π‘Œ))
1315, 100, 48, 130, 51lmod0vs 20741 . . . . . . . . . . . 12 ((π‘Œ ∈ LMod ∧ (π‘ˆβ€˜π‘§) ∈ 𝐡) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = (0gβ€˜π‘Œ))
132126, 129, 131syl2anc 583 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = (0gβ€˜π‘Œ))
133125, 132eqtrd 2766 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) = (0gβ€˜π‘Œ))
13459ad2antrr 723 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ))
13551, 4lss0cl 20794 . . . . . . . . . . 11 ((π‘Œ ∈ LMod ∧ (πΎβ€˜(π‘ˆ β€œ 𝐽)) ∈ (LSubSpβ€˜π‘Œ)) β†’ (0gβ€˜π‘Œ) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
136126, 134, 135syl2anc 583 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ (0gβ€˜π‘Œ) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
137133, 136eqeltrd 2827 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) ∧ Β¬ 𝑧 ∈ 𝐽) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
138105, 137pm2.61dan 810 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((π‘¦β€˜π‘§)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘§)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
13978, 138eqeltrd 2827 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
140139expr 456 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑧 ∈ 𝐼 β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽))))
141140ralrimiv 3139 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ βˆ€π‘§ ∈ 𝐼 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
142 ffnfv 7114 . . . . 5 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢(πΎβ€˜(π‘ˆ β€œ 𝐽)) ↔ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼 ∧ βˆ€π‘§ ∈ 𝐼 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘§) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽))))
14371, 141, 142sylanbrc 582 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢(πΎβ€˜(π‘ˆ β€œ 𝐽)))
1441, 6, 5frlmbasfsupp 21653 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 finSupp 0 )
145144fsuppimpd 9371 . . . . . . 7 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 supp 0 ) ∈ Fin)
14644, 47, 145syl2anc 583 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 supp 0 ) ∈ Fin)
147 dffn2 6713 . . . . . . . . 9 ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) Fn 𝐼 ↔ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢V)
14870, 147sylib 217 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ):𝐼⟢V)
14965adantr 480 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ 𝑦 Fn 𝐼)
15066ad2antrr 723 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ π‘ˆ Fn 𝐼)
151 simpll2 1210 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ 𝐼 ∈ 𝑉)
152 eldifi 4121 . . . . . . . . . . 11 (π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 )) β†’ π‘₯ ∈ 𝐼)
153152adantl 481 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ π‘₯ ∈ 𝐼)
154 fnfvof 7684 . . . . . . . . . 10 (((𝑦 Fn 𝐼 ∧ π‘ˆ Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘₯) = ((π‘¦β€˜π‘₯)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)))
155149, 150, 151, 153, 154syl22anc 836 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘₯) = ((π‘¦β€˜π‘₯)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)))
156 ssidd 4000 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 supp 0 ) βŠ† (𝑦 supp 0 ))
157117a1i 11 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ 0 ∈ V)
15864, 156, 68, 157suppssr 8181 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ (π‘¦β€˜π‘₯) = 0 )
159122ad2antrr 723 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ 0 = (0gβ€˜(Scalarβ€˜π‘Œ)))
160158, 159eqtrd 2766 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ (π‘¦β€˜π‘₯) = (0gβ€˜(Scalarβ€˜π‘Œ)))
161160oveq1d 7420 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((π‘¦β€˜π‘₯)( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)) = ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)))
1623ad2antrr 723 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ π‘Œ ∈ LMod)
16311adantr 480 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ π‘ˆ:𝐼⟢𝐡)
164 ffvelcdm 7077 . . . . . . . . . . 11 ((π‘ˆ:𝐼⟢𝐡 ∧ π‘₯ ∈ 𝐼) β†’ (π‘ˆβ€˜π‘₯) ∈ 𝐡)
165163, 152, 164syl2an 595 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ (π‘ˆβ€˜π‘₯) ∈ 𝐡)
1665, 100, 48, 130, 51lmod0vs 20741 . . . . . . . . . 10 ((π‘Œ ∈ LMod ∧ (π‘ˆβ€˜π‘₯) ∈ 𝐡) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)) = (0gβ€˜π‘Œ))
167162, 165, 166syl2anc 583 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((0gβ€˜(Scalarβ€˜π‘Œ))( ·𝑠 β€˜π‘Œ)(π‘ˆβ€˜π‘₯)) = (0gβ€˜π‘Œ))
168155, 161, 1673eqtrd 2770 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ ∈ (𝐼 βˆ– (𝑦 supp 0 ))) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)β€˜π‘₯) = (0gβ€˜π‘Œ))
169148, 168suppss 8179 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐡) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) βŠ† (𝑦 supp 0 ))
17047, 169syldan 590 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) βŠ† (𝑦 supp 0 ))
171146, 170ssfid 9269 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ ((𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) supp (0gβ€˜π‘Œ)) ∈ Fin)
172 simp2 1134 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ 𝐼 ∈ 𝑉)
1731, 17, 5frlmbasmap 21654 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m 𝐼))
174172, 81, 173syl2an 595 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m 𝐼))
175 elmapfn 8861 . . . . . . . 8 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) β†’ 𝑦 Fn 𝐼)
176174, 175syl 17 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 Fn 𝐼)
17711adantr 480 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ π‘ˆ:𝐼⟢𝐡)
178177ffnd 6712 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ π‘ˆ Fn 𝐼)
179176, 178, 44, 44offun 7681 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ Fun (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ))
180 ovexd 7440 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) ∈ V)
181 fvexd 6900 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (0gβ€˜π‘Œ) ∈ V)
182 funisfsupp 9369 . . . . . 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 257 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ) finSupp (0gβ€˜π‘Œ))
18551, 54, 44, 62, 143, 184gsumsubgcl 19840 . . 3 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ (π‘Œ Ξ£g (𝑦 ∘f ( ·𝑠 β€˜π‘Œ)π‘ˆ)) ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
18650, 185eqeltrd 2827 . 2 (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ (πΎβ€˜(π‘ˆ β€œ 𝐽)))
18742, 186eqelssd 3998 1 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 βŠ† 𝐼) β†’ (πΎβ€˜(π‘ˆ β€œ 𝐽)) = 𝐢)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  {crab 3426  Vcvv 3468   βˆ– cdif 3940   βŠ† wss 3943   class class class wbr 5141  dom cdm 5669  ran crn 5670   β€œ cima 5672  Fun wfun 6531   Fn wfn 6532  βŸΆwf 6533  β€˜cfv 6537  (class class class)co 7405   ∘f cof 7665   supp csupp 8146   ↑m cmap 8822  Fincfn 8941   finSupp cfsupp 9363  Basecbs 17153  Scalarcsca 17209   ·𝑠 cvsca 17210  0gc0g 17394   Ξ£g cgsu 17395  SubGrpcsubg 19047  Abelcabl 19701  Ringcrg 20138  LModclmod 20706  LSubSpclss 20778  LSpanclspn 20818   freeLMod cfrlm 21641   unitVec cuvc 21677
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13491  df-fzo 13634  df-seq 13973  df-hash 14296  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-hom 17230  df-cco 17231  df-0g 17396  df-gsum 17397  df-prds 17402  df-pws 17404  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-mhm 18713  df-submnd 18714  df-grp 18866  df-minusg 18867  df-sbg 18868  df-mulg 18996  df-subg 19050  df-ghm 19139  df-cntz 19233  df-cmn 19702  df-abl 19703  df-mgp 20040  df-rng 20058  df-ur 20087  df-ring 20140  df-subrg 20471  df-lmod 20708  df-lss 20779  df-lsp 20819  df-lmhm 20870  df-sra 21021  df-rgmod 21022  df-dsmm 21627  df-frlm 21642  df-uvc 21678
This theorem is referenced by:  frlmlbs  21692
  Copyright terms: Public domain W3C validator