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 sselid ( 𝜑𝑋 ∈ ( 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 50 ofeqd ( 𝜑 → ∘f ( .r𝐸 ) = ∘f ( ·𝑠𝐴 ) )
409 408 oveqd ( 𝜑 → ( 𝑊f ( .r𝐸 ) 𝐷 ) = ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) )
410 401 407 409 3eqtr2rd ( 𝜑 → ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) = ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) )
411 410 ad2antrr ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) = ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) )
412 411 oveqd ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) = ( 𝑗 ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) 𝑖 ) )
413 simplr ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → 𝑗𝑌 )
414 ovexd ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ∈ V )
415 eqid ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) = ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) )
416 415 ovmpt4g ( ( 𝑗𝑌𝑖𝑋 ∧ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ∈ V ) → ( 𝑗 ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) )
417 413 224 414 416 syl3anc ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( 𝑗 ( 𝑗𝑌 , 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) )
418 412 417 eqtrd ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) )
419 418 mpteq2dva ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) = ( 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) )
420 419 oveq2d ( ( 𝜑𝑗𝑌 ) → ( 𝐸 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) ) )
421 165 adantr ( ( 𝜑𝑗𝑌 ) → 𝐸 ∈ Ring )
422 370 sselda ( ( 𝜑𝑗𝑌 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
423 165 ad2antrr ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → 𝐸 ∈ Ring )
424 387 ad2antrr ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
425 424 222 sseldd ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
426 29 74 ringcl ( ( 𝐸 ∈ Ring ∧ ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ) → ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
427 423 425 242 426 syl3anc ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑖𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
428 315 adantr ( ( 𝜑𝑗𝑌 ) → ( 0g𝐸 ) = ( 0g𝐵 ) )
429 248 353 428 3brtr4d ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) finSupp ( 0g𝐸 ) )
430 29 170 100 74 421 148 422 427 429 gsummulc1 ( ( 𝜑𝑗𝑌 ) → ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ( .r𝐸 ) 𝑗 ) ) ) = ( ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) ( .r𝐸 ) 𝑗 ) )
431 420 430 eqtrd ( ( 𝜑𝑗𝑌 ) → ( 𝐸 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) ( .r𝐸 ) 𝑗 ) )
432 148 mptexd ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ∈ V )
433 24 adantr ( ( 𝜑𝑗𝑌 ) → 𝐴 ∈ LMod )
434 43 adantr ( ( 𝜑𝑗𝑌 ) → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
435 1 432 197 433 434 gsumsra ( ( 𝜑𝑗𝑌 ) → ( 𝐸 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) )
436 148 mptexd ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ∈ V )
437 1 436 197 433 434 gsumsra ( ( 𝜑𝑗𝑌 ) → ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) )
438 437 oveq1d ( ( 𝜑𝑗𝑌 ) → ( ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) ( .r𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) ( .r𝐸 ) 𝑗 ) )
439 50 adantr ( ( 𝜑𝑗𝑌 ) → ( .r𝐸 ) = ( ·𝑠𝐴 ) )
440 350 oveq2d ( ( 𝜑𝑗𝑌 ) → ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) )
441 439 440 356 oveq123d ( ( 𝜑𝑗𝑌 ) → ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) ( .r𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) )
442 438 441 eqtrd ( ( 𝜑𝑗𝑌 ) → ( ( 𝐸 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r𝐸 ) 𝑖 ) ) ) ( .r𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) )
443 431 435 442 3eqtr3d ( ( 𝜑𝑗𝑌 ) → ( 𝐴 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) )
444 443 mpteq2dva ( 𝜑 → ( 𝑗𝑌 ↦ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) ) = ( 𝑗𝑌 ↦ ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) ) )
445 444 oveq2d ( 𝜑 → ( 𝐴 Σg ( 𝑗𝑌 ↦ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( 𝑗 ( 𝑊f ( ·𝑠𝐴 ) 𝐷 ) 𝑖 ) ) ) ) ) = ( 𝐴 Σg ( 𝑗𝑌 ↦ ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) ) ) )
446 383 16 445 3eqtr3rd ( 𝜑 → ( 𝐴 Σg ( 𝑗𝑌 ↦ ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) ) ) = ( 0g𝐴 ) )
447 1 6 20 drgext0g ( 𝜑 → ( 0g𝐸 ) = ( 0g𝐴 ) )
448 446 447 315 3eqtr2d ( 𝜑 → ( 𝐴 Σg ( 𝑗𝑌 ↦ ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) ( ·𝑠𝐴 ) 𝑗 ) ) ) = ( 0g𝐵 ) )
449 1 6 20 5 8 14 drgextgsum ( 𝜑 → ( 𝐸 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 𝐴 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) )
450 2 6 9 4 7 14 drgextgsum ( 𝜑 → ( 𝐸 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) )
451 449 450 eqtr3d ( 𝜑 → ( 𝐴 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) )
452 361 448 451 3eqtr3rd ( 𝜑 → ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) )
453 346 452 eqtrd ( 𝜑 → ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) )
454 breq1 ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ↔ ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
455 nfmpt1 𝑗 ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) )
456 455 nfeq2 𝑗 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) )
457 fveq1 ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( 𝑏𝑗 ) = ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) )
458 457 oveq1d ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) = ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) )
459 458 adantr ( ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ∧ 𝑗𝑌 ) → ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) = ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) )
460 456 459 mpteq2da ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) = ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) )
461 460 oveq2d ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) )
462 461 eqeq1d ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ↔ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) )
463 454 462 anbi12d ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) ↔ ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) ) )
464 eqeq1 ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ↔ ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
465 463 464 imbi12d ( 𝑏 = ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) → ( ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ↔ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) → ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ) )
466 367 lbslinds ( LBasis ‘ 𝐵 ) ⊆ ( LIndS ‘ 𝐵 )
467 466 14 sselid ( 𝜑𝑌 ∈ ( LIndS ‘ 𝐵 ) )
468 eqid ( Base ‘ ( Scalar ‘ 𝐵 ) ) = ( Base ‘ ( Scalar ‘ 𝐵 ) )
469 236 468 322 247 207 323 islinds5 ( ( 𝐵 ∈ LMod ∧ 𝑌 ⊆ ( Base ‘ 𝐵 ) ) → ( 𝑌 ∈ ( LIndS ‘ 𝐵 ) ↔ ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ) )
470 469 biimpa ( ( ( 𝐵 ∈ LMod ∧ 𝑌 ⊆ ( Base ‘ 𝐵 ) ) ∧ 𝑌 ∈ ( LIndS ‘ 𝐵 ) ) → ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
471 211 369 467 470 syl21anc ( 𝜑 → ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( 𝑏𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
472 fvexd ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V )
473 elmapg ( ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ∧ 𝑌 ∈ ( LBasis ‘ 𝐵 ) ) → ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ↔ ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ) )
474 473 biimpar ( ( ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ∧ 𝑌 ∈ ( LBasis ‘ 𝐵 ) ) ∧ ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ) → ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) )
475 472 14 254 474 syl21anc ( 𝜑 → ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) )
476 465 471 475 rspcdva ( 𝜑 → ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗𝑌 ↦ ( ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠𝐵 ) 𝑗 ) ) ) = ( 0g𝐵 ) ) → ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
477 340 453 476 mp2and ( 𝜑 → ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) )
478 fconstmpt ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) = ( 𝑗𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
479 477 478 eqtrdi ( 𝜑 → ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑗𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
480 ovex ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ∈ V
481 480 rgenw 𝑗𝑌 ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ∈ V
482 mpteqb ( ∀ 𝑗𝑌 ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ∈ V → ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑗𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ↔ ∀ 𝑗𝑌 ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
483 481 482 ax-mp ( ( 𝑗𝑌 ↦ ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) ) = ( 𝑗𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ↔ ∀ 𝑗𝑌 ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
484 479 483 sylib ( 𝜑 → ∀ 𝑗𝑌 ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
485 484 r19.21bi ( ( 𝜑𝑗𝑌 ) → ( 𝐵 Σg ( 𝑖𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
486 315 447 316 3eqtr3rd ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g𝐴 ) )
487 486 adantr ( ( 𝜑𝑗𝑌 ) → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g𝐴 ) )
488 205 485 487 3eqtrd ( ( 𝜑𝑗𝑌 ) → ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) )
489 186 488 jca ( ( 𝜑𝑗𝑌 ) → ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) )
490 189 fmpttd ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
491 fvexd ( ( 𝜑𝑗𝑌 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
492 491 148 elmapd ( ( 𝜑𝑗𝑌 ) → ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ↔ ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
493 490 492 mpbird ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) )
494 simpr ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
495 494 breq1d ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
496 nfv 𝑖 ( 𝜑𝑗𝑌 )
497 nfmpt1 𝑖 ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
498 497 nfeq2 𝑖 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
499 496 498 nfan 𝑖 ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
500 simplr ( ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖𝑋 ) → 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
501 500 fveq1d ( ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖𝑋 ) → ( 𝑤𝑖 ) = ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) )
502 501 oveq1d ( ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖𝑋 ) → ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) = ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) )
503 499 502 mpteq2da ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑖𝑋 ↦ ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) = ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) )
504 503 oveq2d ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) )
505 504 eqeq1d ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ↔ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) )
506 495 505 anbi12d ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) ↔ ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) ) )
507 494 eqeq1d ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
508 506 507 imbi12d ( ( ( 𝜑𝑗𝑌 ) ∧ 𝑤 = ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ↔ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) → ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
509 493 508 rspcdv ( ( 𝜑𝑗𝑌 ) → ( ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( 𝑤𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) → ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖𝑋 ↦ ( ( ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠𝐴 ) 𝑖 ) ) ) = ( 0g𝐴 ) ) → ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
510 144 489 509 mp2d ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )
511 510 257 eqtrdi ( ( 𝜑𝑗𝑌 ) → ( 𝑖𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
512 511 311 sylib ( ( 𝜑𝑗𝑌 ) → ∀ 𝑖𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
513 512 ralrimiva ( 𝜑 → ∀ 𝑗𝑌𝑖𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
514 eqidd ( ( 𝑗 = 𝑘𝑖 = 𝑙 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
515 fvexd ( ( 𝜑𝑗𝑌𝑖𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
516 fvexd ( ( 𝜑𝑘𝑌𝑙𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
517 160 514 515 516 fnmpoovd ( 𝜑 → ( 𝑊 = ( 𝑘𝑌 , 𝑙𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑗𝑌𝑖𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
518 513 517 mpbird ( 𝜑𝑊 = ( 𝑘𝑌 , 𝑙𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
519 fconstmpo ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) = ( 𝑘𝑌 , 𝑙𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
520 518 519 eqtr4di ( 𝜑𝑊 = ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )