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 eqtrid ⊢ ( 𝜑 → 𝐾 = ( 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 fovcdmda ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑗 𝑊 𝑖 ) ∈ ( 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 eqtrid ⊢ ( 𝜑 → 𝐹 = ( 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 bitrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 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 ablgrp ⊢ ( 𝐵 ∈ Abel → 𝐵 ∈ Grp )
330 grpmnd ⊢ ( 𝐵 ∈ Grp → 𝐵 ∈ Mnd )
331 211 213 329 330 4syl ⊢ ( 𝜑 → 𝐵 ∈ Mnd )
332 207 gsumz ⊢ ( ( 𝐵 ∈ Mnd ∧ 𝑋 ∈ ( LBasis ‘ 𝐶 ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) = ( 0g ‘ 𝐵 ) )
333 331 13 332 syl2anc ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) = ( 0g ‘ 𝐵 ) )
334 333 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ 𝐵 ) ) ) = ( 0g ‘ 𝐵 ) )
335 316 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 0g ‘ 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
336 328 334 335 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
337 336 14 suppss2 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ⊆ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } )
338 suppssfifsupp ⊢ ( ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∧ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ) ∧ ( { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ∈ Fin ∧ ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ⊆ { 𝑘 ∈ 𝑌 ∣ ( 𝑖 ∈ 𝑋 ↦ ( 𝑘 𝑊 𝑖 ) ) ≠ ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) } ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
339 206 255 256 286 337 338 syl32anc ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
340 eqidd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) )
341 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V )
342 340 341 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) = ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
343 342 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
344 343 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) )
345 344 oveq2d ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
346 124 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐵 ) )
347 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) )
348 347 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) )
349 348 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) )
350 123 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) )
351 350 oveqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) = ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) )
352 351 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) )
353 349 352 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) )
354 353 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
355 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 = 𝑗 )
356 346 354 355 oveq123d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
357 204 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
358 356 357 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) = ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
359 358 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) )
360 359 oveq2d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
361 1 29 sraring ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑉 ⊆ ( Base ‘ 𝐸 ) ) → 𝐴 ∈ Ring )
362 165 43 361 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ Ring )
363 ringcmn ⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ CMnd )
364 362 363 syl ⊢ ( 𝜑 → 𝐴 ∈ CMnd )
365 165 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝐸 ∈ Ring )
366 eqid ⊢ ( LBasis ‘ 𝐵 ) = ( LBasis ‘ 𝐵 )
367 236 366 lbsss ⊢ ( 𝑌 ∈ ( LBasis ‘ 𝐵 ) → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
368 14 367 syl ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
369 368 243 sseqtrrd ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
370 369 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
371 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑗 ∈ 𝑌 )
372 370 371 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
373 29 74 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ∧ 𝑗 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐸 ) )
374 365 241 372 373 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐸 ) )
375 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
376 374 375 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
377 376 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
378 11 fmpo ⊢ ( ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) ↔ 𝐷 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
379 377 378 sylib ⊢ ( 𝜑 → 𝐷 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
380 79 80 82 81 24 159 379 150 lcomf ⊢ ( 𝜑 → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
381 79 80 82 81 24 159 379 150 139 140 163 lcomfsupp ⊢ ( 𝜑 → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) finSupp ( 0g ‘ 𝐴 ) )
382 81 139 364 14 13 380 381 gsumxp ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) ) ) )
383 165 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ Ring )
384 159 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑊 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
385 64 62 eqtrd ⊢ ( 𝜑 → 𝑉 = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
386 385 43 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
387 68 386 eqsstrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐸 ) )
388 387 44 sseqtrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐴 ) )
389 388 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐴 ) )
390 384 389 fssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑊 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
391 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ 𝑌 )
392 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
393 390 391 392 fovcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐴 ) )
394 44 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
395 393 394 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
396 241 3impb ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐸 ) )
397 372 3impb ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
398 29 74 ringass ⊢ ( ( 𝐸 ∈ Ring ∧ ( ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ∧ 𝑗 ∈ ( Base ‘ 𝐸 ) ) ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
399 383 395 396 397 398 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
400 399 mpoeq3dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
401 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ V )
402 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ V )
403 fnov ⊢ ( 𝑊 Fn ( 𝑌 × 𝑋 ) ↔ 𝑊 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
404 160 403 sylib ⊢ ( 𝜑 → 𝑊 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
405 11 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
406 14 13 401 402 404 405 offval22 ⊢ ( 𝜑 → ( 𝑊 ∘f ( .r ‘ 𝐸 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
407 50 ofeqd ⊢ ( 𝜑 → ∘f ( .r ‘ 𝐸 ) = ∘f ( ·𝑠 ‘ 𝐴 ) )
408 407 oveqd ⊢ ( 𝜑 → ( 𝑊 ∘f ( .r ‘ 𝐸 ) 𝐷 ) = ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) )
409 400 406 408 3eqtr2rd ⊢ ( 𝜑 → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) )
410 409 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) )
411 410 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) = ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) 𝑖 ) )
412 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ 𝑌 )
413 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ∈ V )
414 eqid ⊢ ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
415 414 ovmpt4g ⊢ ( ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ∈ V ) → ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
416 412 224 413 415 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
417 411 416 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) = ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) )
418 417 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) )
419 418 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
420 165 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐸 ∈ Ring )
421 369 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
422 165 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ Ring )
423 386 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
424 423 222 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
425 29 74 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ ( 𝑗 𝑊 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
426 422 424 242 425 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
427 315 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐵 ) )
428 248 352 427 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) finSupp ( 0g ‘ 𝐸 ) )
429 29 170 74 420 148 421 426 428 gsummulc1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) ) = ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
430 419 429 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
431 148 mptexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ∈ V )
432 24 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐴 ∈ LMod )
433 43 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
434 1 431 197 432 433 gsumsra ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) )
435 148 mptexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ∈ V )
436 1 435 197 432 433 gsumsra ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) )
437 436 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
438 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) )
439 349 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) )
440 438 439 355 oveq123d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) )
441 437 440 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) )
442 430 434 441 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) = ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) )
443 442 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) )
444 443 oveq2d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝑊 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) 𝑖 ) ) ) ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) )
445 382 16 444 3eqtr3rd ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) = ( 0g ‘ 𝐴 ) )
446 1 6 20 drgext0g ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐴 ) )
447 445 446 315 3eqtr2d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐴 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) )
448 1 6 20 5 8 14 drgextgsum ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
449 2 6 9 4 7 14 drgextgsum ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
450 448 449 eqtr3d ⊢ ( 𝜑 → ( 𝐴 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
451 360 447 450 3eqtr3rd ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) )
452 345 451 eqtrd ⊢ ( 𝜑 → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) )
453 breq1 ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ↔ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
454 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
455 454 nfeq2 ⊢ Ⅎ 𝑗 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) )
456 fveq1 ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 ‘ 𝑗 ) = ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) )
457 456 oveq1d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
458 457 adantr ⊢ ( ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
459 455 458 mpteq2da ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) )
460 459 oveq2d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
461 460 eqeq1d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ↔ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) )
462 453 461 anbi12d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) ↔ ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) ) )
463 eqeq1 ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ↔ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
464 462 463 imbi12d ⊢ ( 𝑏 = ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) → ( ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ↔ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ) )
465 366 lbslinds ⊢ ( LBasis ‘ 𝐵 ) ⊆ ( LIndS ‘ 𝐵 )
466 465 14 sselid ⊢ ( 𝜑 → 𝑌 ∈ ( LIndS ‘ 𝐵 ) )
467 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐵 ) ) = ( Base ‘ ( Scalar ‘ 𝐵 ) )
468 236 467 322 247 207 323 islinds5 ⊢ ( ( 𝐵 ∈ LMod ∧ 𝑌 ⊆ ( Base ‘ 𝐵 ) ) → ( 𝑌 ∈ ( LIndS ‘ 𝐵 ) ↔ ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) ) )
469 468 biimpa ⊢ ( ( ( 𝐵 ∈ LMod ∧ 𝑌 ⊆ ( Base ‘ 𝐵 ) ) ∧ 𝑌 ∈ ( LIndS ‘ 𝐵 ) ) → ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
470 211 368 466 469 syl21anc ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ( ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝑏 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → 𝑏 = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
471 fvexd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V )
472 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ∧ 𝑌 ∈ ( LBasis ‘ 𝐵 ) ) → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) ↔ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ) )
473 472 biimpar ⊢ ( ( ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∈ V ∧ 𝑌 ∈ ( LBasis ‘ 𝐵 ) ) ∧ ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) )
474 471 14 254 473 syl21anc ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐵 ) ) ↑m 𝑌 ) )
475 464 470 474 rspcdva ⊢ ( 𝜑 → ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∧ ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 0g ‘ 𝐵 ) ) → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) ) )
476 339 452 475 mp2and ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) )
477 fconstmpt ⊢ ( 𝑌 × { ( 0g ‘ ( Scalar ‘ 𝐵 ) ) } ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
478 476 477 eqtrdi ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
479 ovex ⊢ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V
480 479 rgenw ⊢ ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V
481 mpteqb ⊢ ( ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ∈ V → ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ↔ ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
482 480 481 ax-mp ⊢ ( ( 𝑗 ∈ 𝑌 ↦ ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ↔ ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
483 478 482 sylib ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
484 483 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐵 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑗 𝑊 𝑖 ) ( ·𝑠 ‘ 𝐵 ) 𝑖 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
485 315 446 316 3eqtr3rd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ 𝐴 ) )
486 485 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ 𝐴 ) )
487 205 484 486 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) )
488 186 487 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) )
489 189 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
490 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
491 490 148 elmapd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
492 489 491 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) )
493 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
494 493 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
495 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ 𝑌 )
496 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
497 496 nfeq2 ⊢ Ⅎ 𝑖 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) )
498 495 497 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
499 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) )
500 499 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑤 ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) )
501 500 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) = ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) )
502 498 501 mpteq2da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) )
503 502 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) )
504 503 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ↔ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) )
505 494 504 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) ↔ ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) ) )
506 493 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ↔ ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) )
507 505 506 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑤 = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ) → ( ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ↔ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
508 492 507 rspcdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ∀ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m 𝑋 ) ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑤 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → 𝑤 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) → ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐴 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐴 ) 𝑖 ) ) ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) ) ) )
509 144 488 508 mp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )
510 509 257 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 𝑊 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
511 510 311 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
512 511 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
513 eqidd ⊢ ( ( 𝑗 = 𝑘 ∧ 𝑖 = 𝑙 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
514 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
515 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋 ) → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
516 160 513 514 515 fnmpoovd ⊢ ( 𝜑 → ( 𝑊 = ( 𝑘 ∈ 𝑌 , 𝑙 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) ↔ ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑗 𝑊 𝑖 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
517 512 516 mpbird ⊢ ( 𝜑 → 𝑊 = ( 𝑘 ∈ 𝑌 , 𝑙 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ) )
518 fconstmpo ⊢ ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) = ( 𝑘 ∈ 𝑌 , 𝑙 ∈ 𝑋 ↦ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
519 517 518 eqtr4di ⊢ ( 𝜑 → 𝑊 = ( ( 𝑌 × 𝑋 ) × { ( 0g ‘ ( Scalar ‘ 𝐴 ) ) } ) )