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 ffvelrnd ( ( ( 𝑅 ∈ 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 ffvelrnd ( ( ( 𝑅 ∈ 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 syl5eq ( ( 𝑅 ∈ 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 ffvelrnda ( ( ( 𝑅 ∈ 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 ffvelrn ( ( 𝑈 : 𝐼𝐵𝑥𝐼 ) → ( 𝑈𝑥 ) ∈ 𝐵 )
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 ∧ 𝐼𝑉𝐽𝐼 ) → ( 𝐾 ‘ ( 𝑈𝐽 ) ) = 𝐶 )