Metamath Proof Explorer

Theorem fedgmullem2

Description: Lemma for fedgmul . (Contributed by Thierry Arnoux, 20-Jul-2023)

Ref Expression
Hypotheses fedgmul.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑉 )
fedgmul.b ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
fedgmul.c ⊢ 𝐶 = ( ( subringAlg ‘ 𝐹 ) ‘ 𝑉 )
fedgmul.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
fedgmul.k ⊢ 𝐾 = ( 𝐸 ↾s 𝑉 )
fedgmul.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
fedgmul.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
fedgmul.3 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
fedgmul.4 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
fedgmul.5 ⊢ ( 𝜑 → 𝑉 ∈ ( SubRing ‘ 𝐹 ) )
fedgmullem.d ⊢ 𝐷 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) )
fedgmullem.h ⊢ 𝐻 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) )
fedgmullem.x ⊢ ( 𝜑 → 𝑋 ∈ ( LBasis ‘ 𝐶 ) )
fedgmullem.y ⊢ ( 𝜑 → 𝑌 ∈ ( LBasis ‘ 𝐵 ) )
fedgmullem2.1 ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) ) )
fedgmullem2.2 ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) = ( 0g ‘ 𝐴 ) )
Assertion fedgmullem2 ( 𝜑 → 𝑊 = ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )

Proof

Step Hyp Ref Expression
1 fedgmul.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑉 )
2 fedgmul.b ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
3 fedgmul.c ⊢ 𝐶 = ( ( subringAlg ‘ 𝐹 ) ‘ 𝑉 )
4 fedgmul.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
5 fedgmul.k ⊢ 𝐾 = ( 𝐸 ↾s 𝑉 )
6 fedgmul.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
7 fedgmul.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
8 fedgmul.3 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
9 fedgmul.4 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
10 fedgmul.5 ⊢ ( 𝜑 → 𝑉 ∈ ( SubRing ‘ 𝐹 ) )
11 fedgmullem.d ⊢ 𝐷 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) )
12 fedgmullem.h ⊢ 𝐻 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) )
13 fedgmullem.x ⊢ ( 𝜑 → 𝑋 ∈ ( LBasis ‘ 𝐶 ) )
14 fedgmullem.y ⊢ ( 𝜑 → 𝑌 ∈ ( LBasis ‘ 𝐵 ) )
15 fedgmullem2.1 ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) ) )
16 fedgmullem2.2 ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) = ( 0g ‘ 𝐴 ) )
17 4 subsubrg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( 𝑉 ∈ ( SubRing ‘ 𝐹 ) ↔ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) ) )
18 17 biimpa ⊢ ( ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ∈ ( SubRing ‘ 𝐹 ) ) → ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) )
19 9 10 18 syl2anc ⊢ ( 𝜑 → ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) )
20 19 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( SubRing ‘ 𝐸 ) )
21 1 5 sralvec ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LVec )
22 6 8 20 21 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ LVec )
23 lveclmod ⊢ ( 𝐴 ∈ LVec → 𝐴 ∈ LMod )
24 22 23 syl ⊢ ( 𝜑 → 𝐴 ∈ LMod )
25 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
26 eqid ⊢ ( LBasis ‘ 𝐶 ) = ( LBasis ‘ 𝐶 )
27 25 26 lbsss ⊢ ( 𝑋 ∈ ( LBasis ‘ 𝐶 ) → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
28 13 27 syl ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
29 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
30 29 subrgss ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
31 9 30 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
32 4 29 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝐸 ) → 𝑈 = ( Base ‘ 𝐹 ) )
33 31 32 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐹 ) )
34 3 a1i ⊢ ( 𝜑 → 𝐶 = ( ( subringAlg ‘ 𝐹 ) ‘ 𝑉 ) )
35 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
36 35 subrgss ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐹 ) → 𝑉 ⊆ ( Base ‘ 𝐹 ) )
37 10 36 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝐹 ) )
38 34 37 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ 𝐶 ) )
39 33 38 eqtrd ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
40 39 31 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ⊆ ( Base ‘ 𝐸 ) )
41 1 a1i ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑉 ) )
42 29 subrgss ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
43 20 42 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
44 41 43 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
45 40 44 sseqtrd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ⊆ ( Base ‘ 𝐴 ) )
46 28 45 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝐴 ) )
47 41 9 43 srasubrg ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐴 ) )
48 subrgsubg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐴 ) → 𝑈 ∈ ( SubGrp ‘ 𝐴 ) )
49 47 48 syl ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐴 ) )
50 1 6 20 drgextvsca ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) )
51 50 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝐸 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) )
52 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
53 19 simprd ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑉 ⊆ 𝑈 )
55 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
56 ressabs ⊢ ( ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝐸 ↾s 𝑈 ) ↾s 𝑉 ) = ( 𝐸 ↾s 𝑉 ) )
57 9 53 56 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ↾s 𝑈 ) ↾s 𝑉 ) = ( 𝐸 ↾s 𝑉 ) )
58 4 oveq1i ⊢ ( 𝐹 ↾s 𝑉 ) = ( ( 𝐸 ↾s 𝑈 ) ↾s 𝑉 )
59 57 58 5 3eqtr4g ⊢ ( 𝜑 → ( 𝐹 ↾s 𝑉 ) = 𝐾 )
60 34 37 srasca ⊢ ( 𝜑 → ( 𝐹 ↾s 𝑉 ) = ( Scalar ‘ 𝐶 ) )
61 59 60 eqtr3d ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝐶 ) )
62 61 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
63 5 29 ressbas2 ⊢ ( 𝑉 ⊆ ( Base ‘ 𝐸 ) → 𝑉 = ( Base ‘ 𝐾 ) )
64 43 63 syl ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝐾 ) )
65 41 43 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝑉 ) = ( Scalar ‘ 𝐴 ) )
66 5 65 syl5eq ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝐴 ) )
67 59 60 66 3eqtr3rd ⊢ ( 𝜑 → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐶 ) )
68 67 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
69 62 64 68 3eqtr4d ⊢ ( 𝜑 → 𝑉 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑉 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
71 55 70 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑉 )
72 54 71 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
73 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
74 eqid ⊢ ( .r ‘ 𝐸 ) = ( .r ‘ 𝐸 )
75 74 subrgmcl ⊢ ( ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝐸 ) 𝑦 ) ∈ 𝑈 )
76 52 72 73 75 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝐸 ) 𝑦 ) ∈ 𝑈 )
77 51 76 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) ∈ 𝑈 )
78 77 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) ∈ 𝑈 )
79 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
80 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
81 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
82 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
83 eqid ⊢ ( LSubSp ‘ 𝐴 ) = ( LSubSp ‘ 𝐴 )
84 79 80 81 82 83 islss4 ⊢ ( 𝐴 ∈ LMod → ( 𝑈 ∈ ( LSubSp ‘ 𝐴 ) ↔ ( 𝑈 ∈ ( SubGrp ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) ∈ 𝑈 ) ) )
85 84 biimpar ⊢ ( ( 𝐴 ∈ LMod ∧ ( 𝑈 ∈ ( SubGrp ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) ∈ 𝑈 ) ) → 𝑈 ∈ ( LSubSp ‘ 𝐴 ) )
86 24 49 78 85 syl12anc ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝐴 ) )
87 28 39 sseqtrrd ⊢ ( 𝜑 → 𝑋 ⊆ 𝑈 )
88 26 lbslinds ⊢ ( LBasis ‘ 𝐶 ) ⊆ ( LIndS ‘ 𝐶 )
89 88 13 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( LIndS ‘ 𝐶 ) )
90 31 44 sseqtrd ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐴 ) )
91 eqid ⊢ ( 𝐴 ↾s 𝑈 ) = ( 𝐴 ↾s 𝑈 )
92 91 81 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝐴 ) → 𝑈 = ( Base ‘ ( 𝐴 ↾s 𝑈 ) ) )
93 90 92 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( 𝐴 ↾s 𝑈 ) ) )
94 33 93 38 3eqtr3rd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ ( 𝐴 ↾s 𝑈 ) ) )
95 91 79 resssca ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( 𝐴 ↾s 𝑈 ) ) )
96 9 95 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( 𝐴 ↾s 𝑈 ) ) )
97 67 96 eqtr3d ⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) = ( Scalar ‘ ( 𝐴 ↾s 𝑈 ) ) )
98 97 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ ( 𝐴 ↾s 𝑈 ) ) ) )
99 97 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ ( Scalar ‘ ( 𝐴 ↾s 𝑈 ) ) ) )
100 eqid ⊢ ( +g ‘ 𝐸 ) = ( +g ‘ 𝐸 )
101 4 100 ressplusg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( +g ‘ 𝐸 ) = ( +g ‘ 𝐹 ) )
102 9 101 syl ⊢ ( 𝜑 → ( +g ‘ 𝐸 ) = ( +g ‘ 𝐹 ) )
103 41 43 sraaddg ⊢ ( 𝜑 → ( +g ‘ 𝐸 ) = ( +g ‘ 𝐴 ) )
104 34 37 sraaddg ⊢ ( 𝜑 → ( +g ‘ 𝐹 ) = ( +g ‘ 𝐶 ) )
105 102 103 104 3eqtr3rd ⊢ ( 𝜑 → ( +g ‘ 𝐶 ) = ( +g ‘ 𝐴 ) )
106 eqid ⊢ ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 )
107 91 106 ressplusg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( +g ‘ 𝐴 ) = ( +g ‘ ( 𝐴 ↾s 𝑈 ) ) )
108 9 107 syl ⊢ ( 𝜑 → ( +g ‘ 𝐴 ) = ( +g ‘ ( 𝐴 ↾s 𝑈 ) ) )
109 105 108 eqtrd ⊢ ( 𝜑 → ( +g ‘ 𝐶 ) = ( +g ‘ ( 𝐴 ↾s 𝑈 ) ) )
110 109 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( +g ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝐴 ↾s 𝑈 ) ) 𝑦 ) )
111 59 8 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ↾s 𝑉 ) ∈ DivRing )
112 eqid ⊢ ( 𝐹 ↾s 𝑉 ) = ( 𝐹 ↾s 𝑉 )
113 3 112 sralvec ⊢ ( ( 𝐹 ∈ DivRing ∧ ( 𝐹 ↾s 𝑉 ) ∈ DivRing ∧ 𝑉 ∈ ( SubRing ‘ 𝐹 ) ) → 𝐶 ∈ LVec )
114 7 111 10 113 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ LVec )
115 lveclmod ⊢ ( 𝐶 ∈ LVec → 𝐶 ∈ LMod )
116 114 115 syl ⊢ ( 𝜑 → 𝐶 ∈ LMod )
117 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
118 eqid ⊢ ( ·𝑠 ‘ 𝐶 ) = ( ·𝑠 ‘ 𝐶 )
119 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
120 25 117 118 119 lmodvscl ⊢ ( ( 𝐶 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐶 ) 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
121 120 3expb ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐶 ) 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
122 116 121 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐶 ) 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
123 2 6 9 drgextvsca ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) )
124 50 123 eqtr3d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐵 ) )
125 91 82 ressvsca ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ( 𝐴 ↾s 𝑈 ) ) )
126 9 125 syl ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ( 𝐴 ↾s 𝑈 ) ) )
127 4 74 ressmulr ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐹 ) )
128 9 127 syl ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐹 ) )
129 3 7 10 drgextvsca ⊢ ( 𝜑 → ( .r ‘ 𝐹 ) = ( ·𝑠 ‘ 𝐶 ) )
130 128 123 129 3eqtr3d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐵 ) = ( ·𝑠 ‘ 𝐶 ) )
131 124 126 130 3eqtr3rd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐶 ) = ( ·𝑠 ‘ ( 𝐴 ↾s 𝑈 ) ) )
132 131 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ ( 𝐴 ↾s 𝑈 ) ) 𝑦 ) )
133 ovexd ⊢ ( 𝜑 → ( 𝐴 ↾s 𝑈 ) ∈ V )
134 94 98 99 110 122 132 114 133 lindspropd ⊢ ( 𝜑 → ( LIndS ‘ 𝐶 ) = ( LIndS ‘ ( 𝐴 ↾s 𝑈 ) ) )
135 89 134 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( LIndS ‘ ( 𝐴 ↾s 𝑈 ) ) )
136 83 91 lsslinds ⊢ ( ( 𝐴 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝐴 ) ∧ 𝑋 ⊆ 𝑈 ) → ( 𝑋 ∈ ( LIndS ‘ ( 𝐴 ↾s 𝑈 ) ) ↔ 𝑋 ∈ ( LIndS ‘ 𝐴 ) ) )
137 136 biimpa ⊢ ( ( ( 𝐴 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝐴 ) ∧ 𝑋 ⊆ 𝑈 ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝐴 ↾s 𝑈 ) ) ) → 𝑋 ∈ ( LIndS ‘ 𝐴 ) )
138 24 86 87 135 137 syl31anc ⊢ ( 𝜑 → 𝑋 ∈ ( LIndS ‘ 𝐴 ) )
139 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
140 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) )
141 81 80 79 82 139 140 islinds5 ⊢ ( ( 𝐴 ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ 𝐴 ) ) → ( 𝑋 ∈ ( LIndS ‘ 𝐴 ) ↔ ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
142 141 biimpa ⊢ ( ( ( 𝐴 ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ 𝐴 ) ) ∧ 𝑋 ∈ ( LIndS ‘ 𝐴 ) ) → ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
143 24 46 138 142 syl21anc ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
144 143 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
145 eqid ⊢ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
146 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 0g ‘ 𝐹 ) ∈ V )
147 14 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑌 ∈ ( LBasis ‘ 𝐵 ) )
148 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑋 ∈ ( LBasis ‘ 𝐶 ) )
149 fvexd ⊢ ( 𝜑 → ( Scalar ‘ 𝐴 ) ∈ V )
150 14 13 xpexd ⊢ ( 𝜑 → ( 𝑌 × 𝑋 ) ∈ V )
151 eqid ⊢ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) = ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) )
152 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) )
153 151 80 140 152 frlmelbas ⊢ ( ( ( Scalar ‘ 𝐴 ) ∈ V ∧ ( 𝑌 × 𝑋 ) ∈ V ) → ( 𝑊 ∈ ( Base ‘ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) ) ↔ ( 𝑊 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) ∧ 𝑊 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ) )
154 149 150 153 syl2anc ⊢ ( 𝜑 → ( 𝑊 ∈ ( Base ‘ ( ( Scalar ‘ 𝐴 ) freeLMod ( 𝑌 × 𝑋 ) ) ) ↔ ( 𝑊 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) ∧ 𝑊 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ) )
155 15 154 mpbid ⊢ ( 𝜑 → ( 𝑊 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) ∧ 𝑊 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
156 155 simpld ⊢ ( 𝜑 → 𝑊 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) )
157 fvexd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
158 157 150 elmapd ⊢ ( 𝜑 → ( 𝑊 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) ↔ 𝑊 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
159 156 158 mpbid ⊢ ( 𝜑 → 𝑊 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
160 159 ffnd ⊢ ( 𝜑 → 𝑊 Fn ( 𝑌 × 𝑋 ) )
161 160 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑊 Fn ( 𝑌 × 𝑋 ) )
162 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 ∈ 𝑌 )
163 155 simprd ⊢ ( 𝜑 → 𝑊 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
164 drngring ⊢ ( 𝐸 ∈ DivRing → 𝐸 ∈ Ring )
165 6 164 syl ⊢ ( 𝜑 → 𝐸 ∈ Ring )
166 ringmnd ⊢ ( 𝐸 ∈ Ring → 𝐸 ∈ Mnd )
167 165 166 syl ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
168 subrgsubg ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) → 𝑉 ∈ ( SubGrp ‘ 𝐸 ) )
169 20 168 syl ⊢ ( 𝜑 → 𝑉 ∈ ( SubGrp ‘ 𝐸 ) )
170 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
171 170 subg0cl ⊢ ( 𝑉 ∈ ( SubGrp ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ 𝑉 )
172 169 171 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝑉 )
173 53 172 sseldd ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝑈 )
174 4 29 170 ress0g ⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ 𝑈 ∧ 𝑈 ⊆ ( Base ‘ 𝐸 ) ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐹 ) )
175 167 173 31 174 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐹 ) )
176 61 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) ) )
177 5 170 subrg0 ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐾 ) )
178 20 177 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐾 ) )
179 67 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) ) )
180 176 178 179 3eqtr4d ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
181 175 180 eqtr3d ⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
182 163 181 breqtrrd ⊢ ( 𝜑 → 𝑊 finSupp ( 0g ‘ 𝐹 ) )
183 182 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑊 finSupp ( 0g ‘ 𝐹 ) )
184 145 146 147 148 161 162 183 fsuppcurry1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ 𝐹 ) )
185 181 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
186 184 185 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
187 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
188 159 fovrnda ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
189 188 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
190 187 189 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) = ( 𝑗 𝑊 𝑖 ) )
191 190 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) )
192 124 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐵 ) )
193 192 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) )
194 191 193 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) )
195 194 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) )
196 195 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
197 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐸 ∈ DivRing )
198 20 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑉 ∈ ( SubRing ‘ 𝐸 ) )
199 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐾 ∈ DivRing )
200 1 197 198 5 199 148 drgextgsum ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
201 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
202 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐹 ∈ DivRing )
203 2 197 201 4 202 148 drgextgsum ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
204 200 203 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
205 196 204 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
206 14 mptexd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ V )
207 eqid ⊢ ( 0g ‘ 𝐵 ) = ( 0g ‘ 𝐵 )
208 2 4 sralvec ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐵 ∈ LVec )
209 6 7 9 208 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ LVec )
210 lveclmod ⊢ ( 𝐵 ∈ LVec → 𝐵 ∈ LMod )
211 209 210 syl ⊢ ( 𝜑 → 𝐵 ∈ LMod )
212 211 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐵 ∈ LMod )
213 lmodabl ⊢ ( 𝐵 ∈ LMod → 𝐵 ∈ Abel )
214 212 213 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐵 ∈ Abel )
215 2 a1i ⊢ ( 𝜑 → 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
216 215 9 31 srasubrg ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐵 ) )
217 subrgsubg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐵 ) → 𝑈 ∈ ( SubGrp ‘ 𝐵 ) )
218 216 217 syl ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐵 ) )
219 218 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑈 ∈ ( SubGrp ‘ 𝐵 ) )
220 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐶 ∈ LMod )
221 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
222 189 221 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
223 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
224 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
225 223 224 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐶 ) )
226 25 117 118 119 lmodvscl ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑖 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ∈ ( Base ‘ 𝐶 ) )
227 220 222 225 226 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ∈ ( Base ‘ 𝐶 ) )
228 130 oveqd ⊢ ( 𝜑 → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) )
229 228 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) )
230 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑈 = ( Base ‘ 𝐶 ) )
231 227 229 230 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ∈ 𝑈 )
232 231 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) : 𝑋 ⟶ 𝑈 )
233 215 31 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝑈 ) = ( Scalar ‘ 𝐵 ) )
234 4 233 syl5eq ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐵 ) )
235 234 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐹 = ( Scalar ‘ 𝐵 ) )
236 eqid ⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
237 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ V )
238 28 40 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝐸 ) )
239 238 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝐸 ) )
240 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑖 ∈ 𝑋 )
241 239 240 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑖 ∈ ( Base ‘ 𝐸 ) )
242 241 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐸 ) )
243 215 31 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐵 ) )
244 243 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐵 ) )
245 242 244 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐵 ) )
246 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
247 eqid ⊢ ( ·𝑠 ‘ 𝐵 ) = ( ·𝑠 ‘ 𝐵 )
248 148 212 235 236 237 245 207 246 247 184 mptscmfsupp0 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) finSupp ( 0g ‘ 𝐵 ) )
249 207 214 148 219 232 248 gsumsubgcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ 𝑈 )
250 234 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
251 33 250 eqtrd ⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
252 251 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑈 = ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
253 249 252 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
254 253 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
255 254 ffund ⊢ ( 𝜑 → Fun ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) )
256 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∈ V )
257 fconstmpt ⊢ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
258 257 eqeq2i ⊢ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
259 ovex ⊢ ( 𝑘 𝑊 𝑖 ) ∈ V
260 259 rgenw ⊢ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) ∈ V
261 mpteqb ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) ∈ V → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
262 260 261 ax-mp ⊢ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
263 258 262 bitri ⊢ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
264 263 necon3abii ⊢ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ¬ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
265 df-ov ⊢ ( 𝑘 𝑊 𝑖 ) = ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ )
266 265 eqcomi ⊢ ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) = ( 𝑘 𝑊 𝑖 )
267 266 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) = ( 𝑘 𝑊 𝑖 ) )
268 267 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
269 268 necon3abid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ¬ ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
270 269 rexbidva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( ∃ 𝑖 ∈ 𝑋 ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ∃ 𝑖 ∈ 𝑋 ¬ ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
271 rexnal ⊢ ( ∃ 𝑖 ∈ 𝑋 ¬ ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ¬ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
272 270 271 bitr2di ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( ¬ ∀ 𝑖 ∈ 𝑋 ( 𝑘 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ∃ 𝑖 ∈ 𝑋 ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
273 264 272 syl5bb ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ∃ 𝑖 ∈ 𝑋 ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
274 273 rabbidva ⊢ ( 𝜑 → { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } = { 𝑘 ∈ 𝑌 ∣ ∃ 𝑖 ∈ 𝑋 ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } )
275 fveq2 ⊢ ( 𝑧 = ⟨ 𝑘 , 𝑖 ⟩ → ( 𝑊 ‘ 𝑧 ) = ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) )
276 275 neeq1d ⊢ ( 𝑧 = ⟨ 𝑘 , 𝑖 ⟩ → ( ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
277 276 dmrab ⊢ dom { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } = { 𝑘 ∈ 𝑌 ∣ ∃ 𝑖 ∈ 𝑋 ( 𝑊 ‘ ⟨ 𝑘 , 𝑖 ⟩ ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) }
278 274 277 eqtr4di ⊢ ( 𝜑 → { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } = dom { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } )
279 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
280 suppvalfn ⊢ ( ( 𝑊 Fn ( 𝑌 × 𝑋 ) ∧ ( 𝑌 × 𝑋 ) ∈ V ∧ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V ) → ( 𝑊 supp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) = { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } )
281 160 150 279 280 syl3anc ⊢ ( 𝜑 → ( 𝑊 supp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) = { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } )
282 163 fsuppimpd ⊢ ( 𝜑 → ( 𝑊 supp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ∈ Fin )
283 281 282 eqeltrrd ⊢ ( 𝜑 → { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ∈ Fin )
284 dmfi ⊢ ( { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ∈ Fin → dom { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ∈ Fin )
285 283 284 syl ⊢ ( 𝜑 → dom { 𝑧 ∈ ( 𝑌 × 𝑋 ) ∣ ( 𝑊 ‘ 𝑧 ) ≠ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ∈ Fin )
286 278 285 eqeltrd ⊢ ( 𝜑 → { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ∈ Fin )
287 nfv ⊢ Ⅎ 𝑖 𝜑
288 nfcv ⊢ Ⅎ 𝑖 𝑌
289 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) )
290 nfcv ⊢ Ⅎ 𝑖 ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } )
291 289 290 nfne ⊢ Ⅎ 𝑖 ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } )
292 291 288 nfrabw ⊢ Ⅎ 𝑖 { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) }
293 288 292 nfdif ⊢ Ⅎ 𝑖 ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } )
294 293 nfcri ⊢ Ⅎ 𝑖 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } )
295 287 294 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) )
296 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) )
297 296 eldifad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → 𝑗 ∈ 𝑌 )
298 296 eldifbd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ¬ 𝑗 ∈ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } )
299 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 𝑊 𝑖 ) = ( 𝑗 𝑊 𝑖 ) )
300 299 mpteq2dv ⊢ ( 𝑘 = 𝑗 → ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
301 300 neeq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
302 301 elrab ⊢ ( 𝑗 ∈ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ↔ ( 𝑗 ∈ 𝑌 ∧ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
303 298 302 sylnib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ¬ ( 𝑗 ∈ 𝑌 ∧ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
304 297 303 mpnanrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ¬ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )
305 nne ⊢ ( ¬ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )
306 304 305 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )
307 306 257 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
308 ovex ⊢ ( 𝑗 𝑊 𝑖 ) ∈ V
309 308 rgenw ⊢ ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) ∈ V
310 mpteqb ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) ∈ V → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
311 309 310 ax-mp ⊢ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
312 307 311 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
313 312 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
314 313 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) )
315 2 6 9 drgext0g ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐵 ) )
316 2 6 9 drgext0gsca ⊢ ( 𝜑 → ( 0g ‘ 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
317 315 180 316 3eqtr3d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
318 317 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
319 318 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) )
320 211 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝐵 ∈ LMod )
321 297 245 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐵 ) )
322 eqid ⊢ ( Scalar ‘ 𝐵 ) = ( Scalar ‘ 𝐵 )
323 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) )
324 236 322 247 323 207 lmod0vs ⊢ ( ( 𝐵 ∈ LMod ∧ 𝑖 ∈ ( Base ‘ 𝐵 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( 0g ‘ 𝐵 ) )
325 320 321 324 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( 0g ‘ 𝐵 ) )
326 314 319 325 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) = ( 0g ‘ 𝐵 ) )
327 295 326 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) )
328 327 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) )
329 211 213 syl ⊢ ( 𝜑 → 𝐵 ∈ Abel )
330 ablgrp ⊢ ( 𝐵 ∈ Abel → 𝐵 ∈ Grp )
331 grpmnd ⊢ ( 𝐵 ∈ Grp → 𝐵 ∈ Mnd )
332 329 330 331 3syl ⊢ ( 𝜑 → 𝐵 ∈ Mnd )
333 207 gsumz ⊢ ( ( 𝐵 ∈ Mnd ∧ 𝑋 ∈ ( LBasis ‘ 𝐶 ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) = ( 0g ‘ 𝐵 ) )
334 332 13 333 syl2anc ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) = ( 0g ‘ 𝐵 ) )
335 334 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) = ( 0g ‘ 𝐵 ) )
336 316 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 0g ‘ 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
337 328 335 336 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
338 337 14 suppss2 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ⊆ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } )
339 suppssfifsupp ⊢ ( ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∧ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ) ∧ ( { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ∈ Fin ∧ ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ⊆ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
340 206 255 256 286 338 339 syl32anc ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
341 eqidd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) )
342 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V )
343 341 342 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
344 343 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
345 344 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) )
346 345 oveq2d ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
347 124 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐵 ) )
348 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) )
349 348 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) )
350 349 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) )
351 123 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) )
352 351 oveqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) )
353 352 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) )
354 350 353 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) )
355 354 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
356 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 = 𝑗 )
357 347 355 356 oveq123d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
358 204 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
359 357 358 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) = ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
360 359 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) )
361 360 oveq2d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
362 1 29 sraring ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑉 ⊆ ( Base ‘ 𝐸 ) ) → 𝐴 ∈ Ring )
363 165 43 362 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ Ring )
364 ringcmn ⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ CMnd )
365 363 364 syl ⊢ ( 𝜑 → 𝐴 ∈ CMnd )
366 165 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝐸 ∈ Ring )
367 eqid ⊢ ( LBasis ‘ 𝐵 ) = ( LBasis ‘ 𝐵 )
368 236 367 lbsss ⊢ ( 𝑌 ∈ ( LBasis ‘ 𝐵 ) → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
369 14 368 syl ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
370 369 243 sseqtrrd ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
371 370 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
372 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑗 ∈ 𝑌 )
373 371 372 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
374 29 74 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ∧ 𝑗 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐸 ) )
375 366 241 373 374 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐸 ) )
376 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
377 375 376 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
378 377 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
379 11 fmpo ⊢ ( ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) ↔ 𝐷 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
380 378 379 sylib ⊢ ( 𝜑 → 𝐷 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
381 79 80 82 81 24 159 380 150 lcomf ⊢ ( 𝜑 → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
382 79 80 82 81 24 159 380 150 139 140 163 lcomfsupp ⊢ ( 𝜑 → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) finSupp ( 0g ‘ 𝐴 ) )
383 81 139 365 14 13 381 382 gsumxp ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) ) ) )
384 165 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ Ring )
385 159 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑊 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
386 64 62 eqtrd ⊢ ( 𝜑 → 𝑉 = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
387 386 43 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
388 68 387 eqsstrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐸 ) )
389 388 44 sseqtrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐴 ) )
390 389 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐴 ) )
391 385 390 fssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑊 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
392 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ 𝑌 )
393 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
394 391 392 393 fovrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐴 ) )
395 44 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
396 394 395 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
397 241 3impb ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐸 ) )
398 373 3impb ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
399 29 74 ringass ⊢ ( ( 𝐸 ∈ Ring ∧ ( ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ∧ 𝑗 ∈ ( Base ‘ 𝐸 ) ) ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
400 384 396 397 398 399 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
401 400 mpoeq3dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
402 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ V )
403 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ V )
404 fnov ⊢ ( 𝑊 Fn ( 𝑌 × 𝑋 ) ↔ 𝑊 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
405 160 404 sylib ⊢ ( 𝜑 → 𝑊 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
406 11 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
407 14 13 402 403 405 406 offval22 ⊢ ( 𝜑 → ( 𝑊 ∘f ( .r ‘ 𝐸 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
408 ofeq ⊢ ( ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) → ∘f ( .r ‘ 𝐸 ) = ∘f ( ·𝑠 ‘ 𝐴 ) )
409 50 408 syl ⊢ ( 𝜑 → ∘f ( .r ‘ 𝐸 ) = ∘f ( ·𝑠 ‘ 𝐴 ) )
410 409 oveqd ⊢ ( 𝜑 → ( 𝑊 ∘f ( .r ‘ 𝐸 ) 𝐷 ) = ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) )
411 401 407 410 3eqtr2rd ⊢ ( 𝜑 → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) )
412 411 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) )
413 412 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) = ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) 𝑖 ) )
414 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ 𝑌 )
415 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ∈ V )
416 eqid ⊢ ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
417 416 ovmpt4g ⊢ ( ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ∈ V ) → ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
418 414 224 415 417 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
419 413 418 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
420 419 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) )
421 420 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
422 165 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐸 ∈ Ring )
423 370 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
424 165 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ Ring )
425 387 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
426 425 222 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
427 29 74 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
428 424 426 242 427 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
429 315 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐵 ) )
430 248 353 429 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) finSupp ( 0g ‘ 𝐸 ) )
431 29 170 100 74 422 148 423 428 430 gsummulc1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) ) = ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
432 421 431 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
433 148 mptexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ∈ V )
434 24 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐴 ∈ LMod )
435 43 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
436 1 433 197 434 435 gsumsra ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) )
437 148 mptexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ∈ V )
438 1 437 197 434 435 gsumsra ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) )
439 438 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
440 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) )
441 350 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) )
442 440 441 356 oveq123d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) )
443 439 442 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) )
444 432 436 443 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) )
445 444 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) )
446 445 oveq2d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) )
447 383 16 446 3eqtr3rd ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) = ( 0g ‘ 𝐴 ) )
448 1 6 20 drgext0g ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐴 ) )
449 447 448 315 3eqtr2d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) )
450 1 6 20 5 8 14 drgextgsum ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
451 2 6 9 4 7 14 drgextgsum ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
452 450 451 eqtr3d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
453 361 449 452 3eqtr3rd ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) )
454 346 453 eqtrd ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) )
455 breq1 ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ↔ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
456 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
457 456 nfeq2 ⊢ Ⅎ 𝑗 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
458 fveq1 ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 ‘ 𝑗 ) = ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) )
459 458 oveq1d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
460 459 adantr ⊢ ( ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
461 457 460 mpteq2da ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) )
462 461 oveq2d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
463 462 eqeq1d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ↔ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) )
464 455 463 anbi12d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) ↔ ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) ) )
465 eqeq1 ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ↔ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
466 464 465 imbi12d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ↔ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ) )
467 367 lbslinds ⊢ ( LBasis ‘ 𝐵 ) ⊆ ( LIndS ‘ 𝐵 )
468 467 14 sseldi ⊢ ( 𝜑 → 𝑌 ∈ ( LIndS ‘ 𝐵 ) )
469 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐵 ) ) = ( Base ‘ ( Scalar ‘ 𝐵 ) )
470 236 469 322 247 207 323 islinds5 ⊢ ( ( 𝐵 ∈ LMod ∧ 𝑌 ⊆ ( Base ‘ 𝐵 ) ) → ( 𝑌 ∈ ( LIndS ‘ 𝐵 ) ↔ ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ) )
471 470 biimpa ⊢ ( ( ( 𝐵 ∈ LMod ∧ 𝑌 ⊆ ( Base ‘ 𝐵 ) ) ∧ 𝑌 ∈ ( LIndS ‘ 𝐵 ) ) → ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
472 211 369 468 471 syl21anc ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
473 fvexd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V )
474 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ∧ 𝑌 ∈ ( LBasis ‘ 𝐵 ) ) → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ↔ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ) )
475 474 biimpar ⊢ ( ( ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ∧ 𝑌 ∈ ( LBasis ‘ 𝐵 ) ) ∧ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) )
476 473 14 254 475 syl21anc ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) )
477 466 472 476 rspcdva ⊢ ( 𝜑 → ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
478 340 454 477 mp2and ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) )
479 fconstmpt ⊢ ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
480 478 479 eqtrdi ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
481 ovex ⊢ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V
482 481 rgenw ⊢ ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V
483 mpteqb ⊢ ( ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ↔ ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
484 482 483 ax-mp ⊢ ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ↔ ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
485 480 484 sylib ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
486 485 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
487 315 448 316 3eqtr3rd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ 𝐴 ) )
488 487 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ 𝐴 ) )
489 205 486 488 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) )
490 186 489 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) )
491 189 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
492 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
493 492 148 elmapd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
494 491 493 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) )
495 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
496 495 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
497 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ 𝑌 )
498 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
499 498 nfeq2 ⊢ Ⅎ 𝑖 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
500 497 499 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
501 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
502 501 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑤 ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) )
503 502 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) = ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) )
504 500 503 mpteq2da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) )
505 504 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) )
506 505 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ↔ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) )
507 496 506 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) ↔ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) ) )
508 495 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
509 507 508 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ↔ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
510 494 509 rspcdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) → ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
511 144 490 510 mp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )
512 511 257 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
513 512 311 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
514 513 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
515 eqidd ⊢ ( ( 𝑗 = 𝑘 ∧ 𝑖 = 𝑙 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
516 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
517 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
518 160 515 516 517 fnmpoovd ⊢ ( 𝜑 → ( 𝑊 = ( 𝑘 ∈ 𝑌 , 𝑙 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
519 514 518 mpbird ⊢ ( 𝜑 → 𝑊 = ( 𝑘 ∈ 𝑌 , 𝑙 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
520 fconstmpo ⊢ ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) = ( 𝑘 ∈ 𝑌 , 𝑙 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
521 519 520 eqtr4di ⊢ ( 𝜑 → 𝑊 = ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )