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 · 𝑈 ) ) )