Metamath Proof Explorer

Theorem uvcresum

Description: Any element of a free module can be expressed as a finite linear combination of unit vectors. (Contributed by Stefan O'Rear, 3-Feb-2015) (Proof shortened by Mario Carneiro, 5-Jul-2015)

Ref Expression
Hypotheses uvcresum.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
uvcresum.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
uvcresum.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
uvcresum.v ⊢ · = ( ·𝑠 ‘ 𝑌 )
Assertion uvcresum ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑌 Σg ( 𝑋 ∘f · 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 uvcresum.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2 uvcresum.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
3 uvcresum.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
4 uvcresum.v ⊢ · = ( ·𝑠 ‘ 𝑌 )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 2 5 3 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
7 6 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
8 7 feqmptd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑎 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑎 ) ) )
9 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → 𝑅 ∈ Ring )
11 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
12 10 11 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → 𝑅 ∈ Mnd )
13 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
14 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ 𝐼 )
15 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
16 7 ffvelcdmda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
17 1 2 3 uvcff ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
18 17 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
19 18 ffvelcdmda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑏 ) ∈ 𝐵 )
20 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21 2 3 5 15 16 19 4 20 frlmvscafval ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) = ( ( 𝐼 × { ( 𝑋 ‘ 𝑏 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑈 ‘ 𝑏 ) ) )
22 16 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) ∧ 𝑎 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
23 2 5 3 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑈 ‘ 𝑏 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝑏 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
24 15 19 23 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑏 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
25 24 ffvelcdmda ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
26 fconstmpt ⊢ ( 𝐼 × { ( 𝑋 ‘ 𝑏 ) } ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑏 ) )
27 26 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝐼 × { ( 𝑋 ‘ 𝑏 ) } ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑏 ) ) )
28 24 feqmptd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑏 ) = ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) )
29 15 22 25 27 28 offval2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝐼 × { ( 𝑋 ‘ 𝑏 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑈 ‘ 𝑏 ) ) = ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) )
30 21 29 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) = ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) )
31 2 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑌 ∈ LMod )
32 31 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑌 ∈ LMod )
33 32 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑌 ∈ LMod )
34 2 frlmsca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝑌 ) )
35 34 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝑌 ) )
36 35 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
37 36 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
38 16 37 eleqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
39 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
40 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
41 3 39 4 40 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑈 ‘ 𝑏 ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) ∈ 𝐵 )
42 33 38 19 41 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) ∈ 𝐵 )
43 30 42 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ∈ 𝐵 )
44 2 5 3 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ∈ 𝐵 ) → ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
45 15 43 44 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
46 45 fvmptelcdm ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐼 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ∈ ( Base ‘ 𝑅 ) )
47 46 an32s ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ∈ ( Base ‘ 𝑅 ) )
48 47 fmpttd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
49 10 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → 𝑅 ∈ Ring )
50 13 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → 𝐼 ∈ 𝑊 )
51 simp2 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → 𝑏 ∈ 𝐼 )
52 14 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → 𝑎 ∈ 𝐼 )
53 simp3 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → 𝑏 ≠ 𝑎 )
54 1 49 50 51 52 53 9 uvcvv0 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) = ( 0g ‘ 𝑅 ) )
55 54 oveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) = ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
56 16 adantlr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
57 56 3adant3 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
58 5 20 9 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
59 49 57 58 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
60 55 59 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑏 ∈ 𝐼 ∧ 𝑏 ≠ 𝑎 ) → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) = ( 0g ‘ 𝑅 ) )
61 60 13 suppsssn ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑎 } )
62 5 9 12 13 14 48 61 gsumpt ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) = ( ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ‘ 𝑎 ) )
63 fveq2 ⊢ ( 𝑏 = 𝑎 → ( 𝑋 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑎 ) )
64 fveq2 ⊢ ( 𝑏 = 𝑎 → ( 𝑈 ‘ 𝑏 ) = ( 𝑈 ‘ 𝑎 ) )
65 64 fveq1d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) )
66 63 65 oveq12d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) = ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) ) )
67 eqid ⊢ ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) = ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) )
68 ovex ⊢ ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) ) ∈ V
69 66 67 68 fvmpt ⊢ ( 𝑎 ∈ 𝐼 → ( ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ‘ 𝑎 ) = ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) ) )
70 69 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ‘ 𝑎 ) = ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) ) )
71 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
72 1 10 13 14 71 uvcvv1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) = ( 1r ‘ 𝑅 ) )
73 72 oveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) ) = ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
74 7 ffvelcdmda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
75 5 20 71 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑋 ‘ 𝑎 ) )
76 10 74 75 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑋 ‘ 𝑎 ) )
77 73 76 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑎 ) ) = ( 𝑋 ‘ 𝑎 ) )
78 70 77 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ‘ 𝑎 ) = ( 𝑋 ‘ 𝑎 ) )
79 62 78 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) = ( 𝑋 ‘ 𝑎 ) )
80 79 mpteq2dva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑎 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑎 ) ) )
81 8 80 eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑎 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ) )
82 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
83 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝐼 ∈ 𝑊 )
84 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
85 mptexg ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ∈ V )
86 85 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ∈ V )
87 funmpt ⊢ Fun ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) )
88 87 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → Fun ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) )
89 fvexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝑌 ) ∈ V )
90 2 9 3 frlmbasfsupp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 finSupp ( 0g ‘ 𝑅 ) )
91 90 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 finSupp ( 0g ‘ 𝑅 ) )
92 91 fsuppimpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ∈ Fin )
93 35 eqcomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑅 )
94 93 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑌 ) ) = ( 0g ‘ 𝑅 ) )
95 94 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 supp ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) = ( 𝑋 supp ( 0g ‘ 𝑅 ) ) )
96 ssid ⊢ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑋 supp ( 0g ‘ 𝑅 ) )
97 95 96 eqsstrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 supp ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) ⊆ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) )
98 fvexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ∈ V )
99 7 97 83 98 suppssr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑋 ‘ 𝑏 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) )
100 99 oveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) · ( 𝑈 ‘ 𝑏 ) ) )
101 eldifi ⊢ ( 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) → 𝑏 ∈ 𝐼 )
102 101 30 sylan2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) = ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) )
103 32 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝑌 ∈ LMod )
104 101 19 sylan2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑈 ‘ 𝑏 ) ∈ 𝐵 )
105 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑌 ) ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) )
106 3 39 4 105 82 lmod0vs ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 ‘ 𝑏 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) · ( 𝑈 ‘ 𝑏 ) ) = ( 0g ‘ 𝑌 ) )
107 103 104 106 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) · ( 𝑈 ‘ 𝑏 ) ) = ( 0g ‘ 𝑌 ) )
108 100 102 107 3eqtr3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) = ( 0g ‘ 𝑌 ) )
109 108 83 suppss2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) supp ( 0g ‘ 𝑌 ) ) ⊆ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) )
110 suppssfifsupp ⊢ ( ( ( ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ∈ V ∧ Fun ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ∧ ( 0g ‘ 𝑌 ) ∈ V ) ∧ ( ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ∧ ( ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) supp ( 0g ‘ 𝑌 ) ) ⊆ ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) finSupp ( 0g ‘ 𝑌 ) )
111 86 88 89 92 109 110 syl32anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) finSupp ( 0g ‘ 𝑌 ) )
112 2 3 82 83 83 84 43 111 frlmgsum ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 Σg ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ) )
113 81 112 eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑌 Σg ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ) )
114 7 feqmptd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑏 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑏 ) ) )
115 18 feqmptd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑈 = ( 𝑏 ∈ 𝐼 ↦ ( 𝑈 ‘ 𝑏 ) ) )
116 83 16 19 114 115 offval2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∘f · 𝑈 ) = ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) ) )
117 30 mpteq2dva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) · ( 𝑈 ‘ 𝑏 ) ) ) = ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) )
118 116 117 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∘f · 𝑈 ) = ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) )
119 118 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 Σg ( 𝑋 ∘f · 𝑈 ) ) = ( 𝑌 Σg ( 𝑏 ∈ 𝐼 ↦ ( 𝑎 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝑏 ) ‘ 𝑎 ) ) ) ) ) )
120 113 119 eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑌 Σg ( 𝑋 ∘f · 𝑈 ) ) )