This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frlmsslsp

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)

Ref Expression
Hypotheses frlmsslsp.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmsslsp.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
frlmsslsp.k ⊢ 𝐾 = ( LSpan ‘ 𝑌 )
frlmsslsp.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
frlmsslsp.z ⊢ 0 = ( 0g ‘ 𝑅 )
frlmsslsp.c ⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
Assertion frlmsslsp ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 frlmsslsp.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmsslsp.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
3 frlmsslsp.k ⊢ 𝐾 = ( LSpan ‘ 𝑌 )
4 frlmsslsp.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
5 frlmsslsp.z ⊢ 0 = ( 0g ‘ 𝑅 )
6 frlmsslsp.c ⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
7 1 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ LMod )
8 7 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑌 ∈ LMod )
9 eqid ⊢ ( LSubSp ‘ 𝑌 ) = ( LSubSp ‘ 𝑌 )
10 1 9 4 5 6 frlmsslss2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ∈ ( LSubSp ‘ 𝑌 ) )
11 2 1 4 uvcff ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
12 11 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
13 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
14 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐽 ⊆ 𝐼 )
15 14 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ∈ 𝐼 )
16 13 15 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑦 ) ∈ 𝐵 )
17 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝐼 ∈ 𝑉 )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 1 18 4 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑈 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝑦 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
20 17 16 19 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑦 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
21 simpll1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑅 ∈ Ring )
22 simpll2 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐼 ∈ 𝑉 )
23 15 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑦 ∈ 𝐼 )
24 eldifi ⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) → 𝑥 ∈ 𝐼 )
25 24 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑥 ∈ 𝐼 )
26 elneeldif ⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑦 ≠ 𝑥 )
27 26 adantll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑦 ≠ 𝑥 )
28 2 21 22 23 25 27 5 uvcvv0 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( ( 𝑈 ‘ 𝑦 ) ‘ 𝑥 ) = 0 )
29 20 28 suppss ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ⊆ 𝐽 )
30 oveq1 ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑦 ) → ( 𝑥 supp 0 ) = ( ( 𝑈 ‘ 𝑦 ) supp 0 ) )
31 30 sseq1d ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑦 ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ⊆ 𝐽 ) )
32 31 6 elrab2 ⊢ ( ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ↔ ( ( 𝑈 ‘ 𝑦 ) ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ⊆ 𝐽 ) )
33 16 29 32 sylanbrc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 )
34 33 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ∀ 𝑦 ∈ 𝐽 ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 )
35 12 ffund ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → Fun 𝑈 )
36 12 fdmd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → dom 𝑈 = 𝐼 )
37 14 36 sseqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐽 ⊆ dom 𝑈 )
38 funimass4 ⊢ ( ( Fun 𝑈 ∧ 𝐽 ⊆ dom 𝑈 ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ) )
39 35 37 38 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ) )
40 34 39 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 “ 𝐽 ) ⊆ 𝐶 )
41 9 3 lspssp ⊢ ( ( 𝑌 ∈ LMod ∧ 𝐶 ∈ ( LSubSp ‘ 𝑌 ) ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ⊆ 𝐶 )
42 8 10 40 41 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ⊆ 𝐶 )
43 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑅 ∈ Ring )
44 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝐼 ∈ 𝑉 )
45 6 ssrab3 ⊢ 𝐶 ⊆ 𝐵
46 45 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ⊆ 𝐵 )
47 46 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐵 )
48 eqid ⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
49 2 1 4 48 uvcresum ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 = ( 𝑌 Σg ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) )
50 43 44 47 49 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 = ( 𝑌 Σg ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) )
51 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
52 lmodabl ⊢ ( 𝑌 ∈ LMod → 𝑌 ∈ Abel )
53 8 52 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑌 ∈ Abel )
54 53 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑌 ∈ Abel )
55 imassrn ⊢ ( 𝑈 “ 𝐽 ) ⊆ ran 𝑈
56 12 frnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ran 𝑈 ⊆ 𝐵 )
57 55 56 sstrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 “ 𝐽 ) ⊆ 𝐵 )
58 4 9 3 lspcl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐵 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) )
59 8 57 58 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) )
60 9 lsssubg ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( SubGrp ‘ 𝑌 ) )
61 8 59 60 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( SubGrp ‘ 𝑌 ) )
62 61 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( SubGrp ‘ 𝑌 ) )
63 1 18 4 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
64 63 3ad2antl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
65 64 ffnd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 Fn 𝐼 )
66 12 ffnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑈 Fn 𝐼 )
67 66 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑈 Fn 𝐼 )
68 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
69 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
70 65 67 68 68 69 offn ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 )
71 47 70 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 )
72 47 65 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 Fn 𝐼 )
73 72 adantrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑦 Fn 𝐼 )
74 66 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑈 Fn 𝐼 )
75 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝐼 ∈ 𝑉 )
76 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑧 ∈ 𝐼 )
77 fnfvof ⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝑈 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) = ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) )
78 73 74 75 76 77 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) = ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) )
79 8 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → 𝑌 ∈ LMod )
80 59 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) )
81 45 sseli ⊢ ( 𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐵 )
82 81 64 sylan2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
83 82 adantrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
84 14 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ∈ 𝐼 )
85 84 adantrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → 𝑧 ∈ 𝐼 )
86 83 85 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑦 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
87 1 frlmsca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝑌 ) )
88 87 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑅 = ( Scalar ‘ 𝑌 ) )
89 88 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
90 89 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
91 86 90 eleqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑦 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
92 4 3 lspssid ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐵 ) → ( 𝑈 “ 𝐽 ) ⊆ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
93 8 57 92 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 “ 𝐽 ) ⊆ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
94 93 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑈 “ 𝐽 ) ⊆ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
95 funfvima2 ⊢ ( ( Fun 𝑈 ∧ 𝐽 ⊆ dom 𝑈 ) → ( 𝑧 ∈ 𝐽 → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) ) )
96 35 37 95 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑧 ∈ 𝐽 → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) ) )
97 96 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) )
98 97 adantrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) )
99 94 98 sseldd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
100 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
101 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
102 100 48 101 9 lssvscl ⊢ ( ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) ∧ ( ( 𝑦 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑈 ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
103 79 80 91 99 102 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
104 103 anassrs ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
105 104 adantlrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
106 id ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) )
107 106 adantrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) )
108 107 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) )
109 simplrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 𝑧 ∈ 𝐼 )
110 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ¬ 𝑧 ∈ 𝐽 )
111 109 110 eldifd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 𝑧 ∈ ( 𝐼 ∖ 𝐽 ) )
112 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 supp 0 ) = ( 𝑦 supp 0 ) )
113 112 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( 𝑦 supp 0 ) ⊆ 𝐽 ) )
114 113 6 elrab2 ⊢ ( 𝑦 ∈ 𝐶 ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 supp 0 ) ⊆ 𝐽 ) )
115 114 simprbi ⊢ ( 𝑦 ∈ 𝐶 → ( 𝑦 supp 0 ) ⊆ 𝐽 )
116 115 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 supp 0 ) ⊆ 𝐽 )
117 5 fvexi ⊢ 0 ∈ V
118 117 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 0 ∈ V )
119 82 116 44 118 suppssr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝑦 ‘ 𝑧 ) = 0 )
120 108 111 119 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝑦 ‘ 𝑧 ) = 0 )
121 88 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
122 5 121 eqtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
123 122 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
124 120 123 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝑦 ‘ 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
125 124 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) )
126 8 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 𝑌 ∈ LMod )
127 12 ffvelcdmda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 )
128 127 adantrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 )
129 128 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 )
130 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑌 ) ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) )
131 4 100 48 130 51 lmod0vs ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( 0g ‘ 𝑌 ) )
132 126 129 131 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( 0g ‘ 𝑌 ) )
133 125 132 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( 0g ‘ 𝑌 ) )
134 59 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) )
135 51 9 lss0cl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) → ( 0g ‘ 𝑌 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
136 126 134 135 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 0g ‘ 𝑌 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
137 133 136 eqeltrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
138 105 137 pm2.61dan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
139 78 138 eqeltrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
140 139 expr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑧 ∈ 𝐼 → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) )
141 140 ralrimiv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ∀ 𝑧 ∈ 𝐼 ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
142 ffnfv ⊢ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ↔ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 ∧ ∀ 𝑧 ∈ 𝐼 ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) )
143 71 141 142 sylanbrc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
144 1 5 4 frlmbasfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 finSupp 0 )
145 144 fsuppimpd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 supp 0 ) ∈ Fin )
146 44 47 145 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 supp 0 ) ∈ Fin )
147 dffn2 ⊢ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 ↔ ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ V )
148 70 147 sylib ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ V )
149 65 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑦 Fn 𝐼 )
150 66 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑈 Fn 𝐼 )
151 simpll2 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝐼 ∈ 𝑉 )
152 eldifi ⊢ ( 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) → 𝑥 ∈ 𝐼 )
153 152 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑥 ∈ 𝐼 )
154 fnfvof ⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝑈 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) )
155 149 150 151 153 154 syl22anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) )
156 ssidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 supp 0 ) ⊆ ( 𝑦 supp 0 ) )
157 117 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 0 ∈ V )
158 64 156 68 157 suppssr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( 𝑦 ‘ 𝑥 ) = 0 )
159 122 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
160 158 159 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( 𝑦 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
161 160 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 𝑦 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) )
162 8 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑌 ∈ LMod )
163 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
164 ffvelcdm ⊢ ( ( 𝑈 : 𝐼 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑥 ) ∈ 𝐵 )
165 163 152 164 syl2an ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( 𝑈 ‘ 𝑥 ) ∈ 𝐵 )
166 4 100 48 130 51 lmod0vs ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) )
167 162 165 166 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) )
168 155 161 167 3eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) )
169 148 168 suppss ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ⊆ ( 𝑦 supp 0 ) )
170 47 169 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ⊆ ( 𝑦 supp 0 ) )
171 146 170 ssfid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ∈ Fin )
172 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐼 ∈ 𝑉 )
173 1 18 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
174 172 81 173 syl2an ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
175 elmapfn ⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) → 𝑦 Fn 𝐼 )
176 174 175 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 Fn 𝐼 )
177 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
178 177 ffnd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑈 Fn 𝐼 )
179 176 178 44 44 offun ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → Fun ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) )
180 ovexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ∈ V )
181 fvexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 0g ‘ 𝑌 ) ∈ V )
182 funisfsupp ⊢ ( ( Fun ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ∧ ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ∈ V ∧ ( 0g ‘ 𝑌 ) ∈ V ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) finSupp ( 0g ‘ 𝑌 ) ↔ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ∈ Fin ) )
183 179 180 181 182 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) finSupp ( 0g ‘ 𝑌 ) ↔ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ∈ Fin ) )
184 171 183 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) finSupp ( 0g ‘ 𝑌 ) )
185 51 54 44 62 143 184 gsumsubgcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑌 Σg ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
186 50 185 eqeltrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) )
187 42 186 eqelssd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) = 𝐶 )