Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fedgmullem2 Structured version   Visualization version   GIF version

Theorem fedgmullem2 32325
Description: Lemma for fedgmul 32326. (Contributed by Thierry Arnoux, 20-Jul-2023.)
Hypotheses
Ref Expression
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
Ref Expression
fedgmullem2 (𝜑𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))
Distinct variable groups:   𝐴,𝑖,𝑗   𝐵,𝑖,𝑗   𝐶,𝑖   𝐷,𝑖,𝑗   𝑖,𝐸,𝑗   𝑈,𝑖   𝑖,𝑊,𝑗   𝑖,𝑋,𝑗   𝑖,𝑌,𝑗   𝜑,𝑖,𝑗
Allowed substitution hints:   𝐶(𝑗)   𝑈(𝑗)   𝐹(𝑖,𝑗)   𝐺(𝑖,𝑗)   𝐻(𝑖,𝑗)   𝐾(𝑖,𝑗)   𝑉(𝑖,𝑗)

Proof of Theorem fedgmullem2
Dummy variables 𝑏 𝑤 𝑘 𝑥 𝑙 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fedgmul.1 . . . . . . . . . . 11 (𝜑𝐸 ∈ DivRing)
2 fedgmul.3 . . . . . . . . . . 11 (𝜑𝐾 ∈ DivRing)
3 fedgmul.4 . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (SubRing‘𝐸))
4 fedgmul.5 . . . . . . . . . . . . 13 (𝜑𝑉 ∈ (SubRing‘𝐹))
5 fedgmul.f . . . . . . . . . . . . . . 15 𝐹 = (𝐸s 𝑈)
65subsubrg 20248 . . . . . . . . . . . . . 14 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
76biimpa 477 . . . . . . . . . . . . 13 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
83, 4, 7syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
98simpld 495 . . . . . . . . . . 11 (𝜑𝑉 ∈ (SubRing‘𝐸))
10 fedgmul.a . . . . . . . . . . . 12 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11 fedgmul.k . . . . . . . . . . . 12 𝐾 = (𝐸s 𝑉)
1210, 11sralvec 32289 . . . . . . . . . . 11 ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
131, 2, 9, 12syl3anc 1371 . . . . . . . . . 10 (𝜑𝐴 ∈ LVec)
14 lveclmod 20567 . . . . . . . . . 10 (𝐴 ∈ LVec → 𝐴 ∈ LMod)
1513, 14syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ LMod)
16 fedgmullem.x . . . . . . . . . . 11 (𝜑𝑋 ∈ (LBasis‘𝐶))
17 eqid 2736 . . . . . . . . . . . 12 (Base‘𝐶) = (Base‘𝐶)
18 eqid 2736 . . . . . . . . . . . 12 (LBasis‘𝐶) = (LBasis‘𝐶)
1917, 18lbsss 20538 . . . . . . . . . . 11 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
2016, 19syl 17 . . . . . . . . . 10 (𝜑𝑋 ⊆ (Base‘𝐶))
21 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2221subrgss 20223 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
233, 22syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
245, 21ressbas2 17120 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘𝐹))
26 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
2726a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
2928subrgss 20223 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
304, 29syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3127, 30srabase 20640 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
3225, 31eqtrd 2776 . . . . . . . . . . . 12 (𝜑𝑈 = (Base‘𝐶))
3332, 23eqsstrrd 3983 . . . . . . . . . . 11 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
3410a1i 11 . . . . . . . . . . . 12 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
3521subrgss 20223 . . . . . . . . . . . . 13 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
369, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑉 ⊆ (Base‘𝐸))
3734, 36srabase 20640 . . . . . . . . . . 11 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
3833, 37sseqtrd 3984 . . . . . . . . . 10 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
3920, 38sstrd 3954 . . . . . . . . 9 (𝜑𝑋 ⊆ (Base‘𝐴))
4034, 3, 36srasubrg 32288 . . . . . . . . . . . 12 (𝜑𝑈 ∈ (SubRing‘𝐴))
41 subrgsubg 20228 . . . . . . . . . . . 12 (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
4240, 41syl 17 . . . . . . . . . . 11 (𝜑𝑈 ∈ (SubGrp‘𝐴))
4310, 1, 9drgextvsca 32292 . . . . . . . . . . . . . 14 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
4443oveqdr 7385 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) = (𝑥( ·𝑠𝐴)𝑦))
453adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
468simprd 496 . . . . . . . . . . . . . . . 16 (𝜑𝑉𝑈)
4746adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉𝑈)
48 simprl 769 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49 ressabs 17130 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
503, 46, 49syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
515oveq1i 7367 . . . . . . . . . . . . . . . . . . . . 21 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
5250, 51, 113eqtr4g 2801 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = 𝐾)
5327, 30srasca 20646 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
5452, 53eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 = (Scalar‘𝐶))
5554fveq2d 6846 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
5611, 21ressbas2 17120 . . . . . . . . . . . . . . . . . . 19 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
5736, 56syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉 = (Base‘𝐾))
5834, 36srasca 20646 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
5911, 58eqtrid 2788 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 = (Scalar‘𝐴))
6052, 53, 593eqtr3rd 2785 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
6160fveq2d 6846 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
6255, 57, 613eqtr4d 2786 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 = (Base‘(Scalar‘𝐴)))
6362adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
6448, 63eleqtrrd 2841 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑉)
6547, 64sseldd 3945 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑈)
66 simprr 771 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑦𝑈)
67 eqid 2736 . . . . . . . . . . . . . . 15 (.r𝐸) = (.r𝐸)
6867subrgmcl 20234 . . . . . . . . . . . . . 14 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥𝑈𝑦𝑈) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
6945, 65, 66, 68syl3anc 1371 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
7044, 69eqeltrrd 2839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
7170ralrimivva 3197 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
72 eqid 2736 . . . . . . . . . . . . 13 (Scalar‘𝐴) = (Scalar‘𝐴)
73 eqid 2736 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74 eqid 2736 . . . . . . . . . . . . 13 (Base‘𝐴) = (Base‘𝐴)
75 eqid 2736 . . . . . . . . . . . . 13 ( ·𝑠𝐴) = ( ·𝑠𝐴)
76 eqid 2736 . . . . . . . . . . . . 13 (LSubSp‘𝐴) = (LSubSp‘𝐴)
7772, 73, 74, 75, 76islss4 20423 . . . . . . . . . . . 12 (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)))
7877biimpar 478 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
7915, 42, 71, 78syl12anc 835 . . . . . . . . . 10 (𝜑𝑈 ∈ (LSubSp‘𝐴))
8020, 32sseqtrrd 3985 . . . . . . . . . 10 (𝜑𝑋𝑈)
8118lbslinds 21239 . . . . . . . . . . . 12 (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
8281, 16sselid 3942 . . . . . . . . . . 11 (𝜑𝑋 ∈ (LIndS‘𝐶))
8323, 37sseqtrd 3984 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐴))
84 eqid 2736 . . . . . . . . . . . . . . 15 (𝐴s 𝑈) = (𝐴s 𝑈)
8584, 74ressbas2 17120 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴s 𝑈)))
8683, 85syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘(𝐴s 𝑈)))
8725, 86, 313eqtr3rd 2785 . . . . . . . . . . . 12 (𝜑 → (Base‘𝐶) = (Base‘(𝐴s 𝑈)))
8884, 72resssca 17224 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
893, 88syl 17 . . . . . . . . . . . . . 14 (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
9060, 89eqtr3d 2778 . . . . . . . . . . . . 13 (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴s 𝑈)))
9190fveq2d 6846 . . . . . . . . . . . 12 (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴s 𝑈))))
9290fveq2d 6846 . . . . . . . . . . . 12 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘(𝐴s 𝑈))))
93 eqid 2736 . . . . . . . . . . . . . . . . 17 (+g𝐸) = (+g𝐸)
945, 93ressplusg 17171 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐸) = (+g𝐹))
953, 94syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐹))
9634, 36sraaddg 20642 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐴))
9727, 30sraaddg 20642 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐹) = (+g𝐶))
9895, 96, 973eqtr3rd 2785 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐶) = (+g𝐴))
99 eqid 2736 . . . . . . . . . . . . . . . 16 (+g𝐴) = (+g𝐴)
10084, 99ressplusg 17171 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐴) = (+g‘(𝐴s 𝑈)))
1013, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐴) = (+g‘(𝐴s 𝑈)))
10298, 101eqtrd 2776 . . . . . . . . . . . . 13 (𝜑 → (+g𝐶) = (+g‘(𝐴s 𝑈)))
103102oveqdr 7385 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g𝐶)𝑦) = (𝑥(+g‘(𝐴s 𝑈))𝑦))
104 fedgmul.2 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ DivRing)
10552, 2eqeltrd 2838 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
106 eqid 2736 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
10726, 106sralvec 32289 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108104, 105, 4, 107syl3anc 1371 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
109 lveclmod 20567 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110108, 109syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
111 eqid 2736 . . . . . . . . . . . . . . 15 (Scalar‘𝐶) = (Scalar‘𝐶)
112 eqid 2736 . . . . . . . . . . . . . . 15 ( ·𝑠𝐶) = ( ·𝑠𝐶)
113 eqid 2736 . . . . . . . . . . . . . . 15 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
11417, 111, 112, 113lmodvscl 20339 . . . . . . . . . . . . . 14 ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
1151143expb 1120 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
116110, 115sylan 580 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
117 fedgmul.b . . . . . . . . . . . . . . . 16 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118117, 1, 3drgextvsca 32292 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
11943, 118eqtr3d 2778 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠𝐵))
12084, 75ressvsca 17225 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1213, 120syl 17 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1225, 67ressmulr 17188 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
1233, 122syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = (.r𝐹))
12426, 104, 4drgextvsca 32292 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
125123, 118, 1243eqtr3d 2784 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐵) = ( ·𝑠𝐶))
126119, 121, 1253eqtr3rd 2785 . . . . . . . . . . . . 13 (𝜑 → ( ·𝑠𝐶) = ( ·𝑠 ‘(𝐴s 𝑈)))
127126oveqdr 7385 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) = (𝑥( ·𝑠 ‘(𝐴s 𝑈))𝑦))
128 ovexd 7392 . . . . . . . . . . . 12 (𝜑 → (𝐴s 𝑈) ∈ V)
12987, 91, 92, 103, 116, 127, 108, 128lindspropd 32170 . . . . . . . . . . 11 (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴s 𝑈)))
13082, 129eleqtrd 2840 . . . . . . . . . 10 (𝜑𝑋 ∈ (LIndS‘(𝐴s 𝑈)))
13176, 84lsslinds 21237 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) → (𝑋 ∈ (LIndS‘(𝐴s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132131biimpa 477 . . . . . . . . . 10 (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
13315, 79, 80, 130, 132syl31anc 1373 . . . . . . . . 9 (𝜑𝑋 ∈ (LIndS‘𝐴))
134 eqid 2736 . . . . . . . . . . 11 (0g𝐴) = (0g𝐴)
135 eqid 2736 . . . . . . . . . . 11 (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
13674, 73, 72, 75, 134, 135islinds5 32156 . . . . . . . . . 10 ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
137136biimpa 477 . . . . . . . . 9 (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
13815, 39, 133, 137syl21anc 836 . . . . . . . 8 (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
139138adantr 481 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
140 eqid 2736 . . . . . . . . . 10 (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
141 fvexd 6857 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (0g𝐹) ∈ V)
142 fedgmullem.y . . . . . . . . . . 11 (𝜑𝑌 ∈ (LBasis‘𝐵))
143142adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑌 ∈ (LBasis‘𝐵))
14416adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145 fedgmullem2.1 . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146 fvexd 6857 . . . . . . . . . . . . . . . 16 (𝜑 → (Scalar‘𝐴) ∈ V)
147142, 16xpexd 7685 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 × 𝑋) ∈ V)
148 eqid 2736 . . . . . . . . . . . . . . . . 17 ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149 eqid 2736 . . . . . . . . . . . . . . . . 17 (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150148, 73, 135, 149frlmelbas 21162 . . . . . . . . . . . . . . . 16 (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
151146, 147, 150syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
152145, 151mpbid 231 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴))))
153152simpld 495 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
154 fvexd 6857 . . . . . . . . . . . . . 14 (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155154, 147elmapd 8779 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156153, 155mpbid 231 . . . . . . . . . . . 12 (𝜑𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157156ffnd 6669 . . . . . . . . . . 11 (𝜑𝑊 Fn (𝑌 × 𝑋))
158157adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159 simpr 485 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑗𝑌)
160152simprd 496 . . . . . . . . . . . 12 (𝜑𝑊 finSupp (0g‘(Scalar‘𝐴)))
161 drngring 20192 . . . . . . . . . . . . . . . 16 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
1621, 161syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ Ring)
163 ringmnd 19974 . . . . . . . . . . . . . . 15 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164162, 163syl 17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ Mnd)
165 subrgsubg 20228 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
1669, 165syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑉 ∈ (SubGrp‘𝐸))
167 eqid 2736 . . . . . . . . . . . . . . . . 17 (0g𝐸) = (0g𝐸)
168167subg0cl 18936 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (SubGrp‘𝐸) → (0g𝐸) ∈ 𝑉)
169166, 168syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0g𝐸) ∈ 𝑉)
17046, 169sseldd 3945 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) ∈ 𝑈)
1715, 21, 167ress0g 18584 . . . . . . . . . . . . . 14 ((𝐸 ∈ Mnd ∧ (0g𝐸) ∈ 𝑈𝑈 ⊆ (Base‘𝐸)) → (0g𝐸) = (0g𝐹))
172164, 170, 23, 171syl3anc 1371 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g𝐹))
17354fveq2d 6846 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
17411, 167subrg0 20229 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
1759, 174syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) = (0g𝐾))
17660fveq2d 6846 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
177173, 175, 1763eqtr4d 2786 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
178172, 177eqtr3d 2778 . . . . . . . . . . . 12 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐴)))
179160, 178breqtrrd 5133 . . . . . . . . . . 11 (𝜑𝑊 finSupp (0g𝐹))
180179adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 finSupp (0g𝐹))
181140, 141, 143, 144, 158, 159, 180fsuppcurry1 31642 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g𝐹))
182178adantr 481 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g𝐹) = (0g‘(Scalar‘𝐴)))
183181, 182breqtrd 5131 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)))
184 eqidd 2737 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
185156fovcdmda 7525 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186185anassrs 468 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187184, 186fvmpt2d 6961 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188187oveq1d 7372 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
189119ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
190189oveqd 7374 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
191188, 190eqtrd 2776 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
192191mpteq2dva 5205 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
193192oveq2d 7373 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1941adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐸 ∈ DivRing)
1959adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑉 ∈ (SubRing‘𝐸))
1962adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐾 ∈ DivRing)
19710, 194, 195, 11, 196, 144drgextgsum 32296 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1983adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199104adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐹 ∈ DivRing)
200117, 194, 198, 5, 199, 144drgextgsum 32296 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
201197, 200eqtr3d 2778 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
202193, 201eqtrd 2776 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
203142mptexd 7174 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ V)
204 eqid 2736 . . . . . . . . . . . . . . . . . 18 (0g𝐵) = (0g𝐵)
205117, 5sralvec 32289 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
2061, 104, 3, 205syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ LVec)
207 lveclmod 20567 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ LMod)
209208adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐵 ∈ LMod)
210 lmodabl 20369 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝐵 ∈ Abel)
212117a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213212, 3, 23srasubrg 32288 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ (SubRing‘𝐵))
214 subrgsubg 20228 . . . . . . . . . . . . . . . . . . . 20 (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215213, 214syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 ∈ (SubGrp‘𝐵))
216215adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217110ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
21861ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219186, 218eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
22020ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
221 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
222220, 221sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
22317, 111, 112, 113lmodvscl 20339 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
224217, 219, 222, 223syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
225125oveqd 7374 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
226225ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
22732ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
228224, 226, 2273eltr4d 2853 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) ∈ 𝑈)
229228fmpttd 7063 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)):𝑋𝑈)
230212, 23srasca 20646 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
2315, 230eqtrid 2788 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 = (Scalar‘𝐵))
232231adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐹 = (Scalar‘𝐵))
233 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (Base‘𝐵) = (Base‘𝐵)
234 ovexd 7392 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
23520, 33sstrd 3954 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ⊆ (Base‘𝐸))
236235adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237 simprr 771 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
238236, 237sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖 ∈ (Base‘𝐸))
239238anassrs 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
240212, 23srabase 20640 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241240ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐵))
242239, 241eleqtrd 2840 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
243 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (0g𝐹) = (0g𝐹)
244 eqid 2736 . . . . . . . . . . . . . . . . . . 19 ( ·𝑠𝐵) = ( ·𝑠𝐵)
245144, 209, 232, 233, 234, 242, 204, 243, 244, 181mptscmfsupp0 20387 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) finSupp (0g𝐵))
246204, 211, 144, 216, 229, 245gsumsubgcl 19697 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ 𝑈)
247231fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
24825, 247eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘(Scalar‘𝐵)))
249248adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250246, 249eleqtrd 2840 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251250fmpttd 7063 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252251ffund 6672 . . . . . . . . . . . . . 14 (𝜑 → Fun (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
253 fvexd 6857 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
254 fconstmpt 5694 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × {(0g‘(Scalar‘𝐴))}) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴)))
255254eqeq2i 2749 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
256 ovex 7390 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑊𝑖) ∈ V
257256rgenw 3068 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑋 (𝑘𝑊𝑖) ∈ V
258 mpteqb 6967 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑖𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
259257, 258ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
260255, 259bitri 274 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
261260necon3abii 2990 . . . . . . . . . . . . . . . . . 18 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
262 df-ov 7360 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263262eqcomi 2745 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264263a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265264eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
266265necon3abid 2980 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
267266rexbidva 3173 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
268 rexnal 3103 . . . . . . . . . . . . . . . . . . 19 (∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
269267, 268bitr2di 287 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
270261, 269bitrid 282 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑌) → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
271270rabbidva 3414 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))})
272 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273272neeq1d 3003 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊𝑧) ≠ (0g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
274273dmrab 31425 . . . . . . . . . . . . . . . 16 dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))}
275271, 274eqtr4di 2794 . . . . . . . . . . . . . . 15 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
276 fvexd 6857 . . . . . . . . . . . . . . . . . 18 (𝜑 → (0g‘(Scalar‘𝐴)) ∈ V)
277 suppvalfn 8100 . . . . . . . . . . . . . . . . . 18 ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
278157, 147, 276, 277syl3anc 1371 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
279160fsuppimpd 9312 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) ∈ Fin)
280278, 279eqeltrrd 2839 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
281 dmfi 9274 . . . . . . . . . . . . . . . 16 ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
282280, 281syl 17 . . . . . . . . . . . . . . 15 (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
283275, 282eqeltrd 2838 . . . . . . . . . . . . . 14 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin)
284 nfv 1917 . . . . . . . . . . . . . . . . . . 19 𝑖𝜑
285 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑌
286 nfmpt1 5213 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖))
287 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑋 × {(0g‘(Scalar‘𝐴))})
288286, 287nfne 3045 . . . . . . . . . . . . . . . . . . . . . 22 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})
289288, 285nfrabw 3440 . . . . . . . . . . . . . . . . . . . . 21 𝑖{𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}
290285, 289nfdif 4085 . . . . . . . . . . . . . . . . . . . 20 𝑖(𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
291290nfcri 2894 . . . . . . . . . . . . . . . . . . 19 𝑖 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
292284, 291nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑖(𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
293 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
294293eldifad 3922 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗𝑌)
295293eldifbd 3923 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
296 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297296mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑗 → (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
298297neeq1d 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑗 → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
299298elrab 3645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ↔ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
300295, 299sylnib 327 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
301294, 300mpnanrd 410 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}))
302 nne 2947 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
303301, 302sylib 217 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
304303, 254eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
305 ovex 7390 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑊𝑖) ∈ V
306305rgenw 3068 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖𝑋 (𝑗𝑊𝑖) ∈ V
307 mpteqb 6967 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
308306, 307ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
309304, 308sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
310309r19.21bi 3234 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
311310oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖))
312117, 1, 3drgext0g 32291 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐸) = (0g𝐵))
313117, 1, 3drgext0gsca 32293 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐵) = (0g‘(Scalar‘𝐵)))
314312, 177, 3133eqtr3d 2784 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
315314ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
316315oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖))
317208ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝐵 ∈ LMod)
318294, 242syldanl 602 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
319 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (Scalar‘𝐵) = (Scalar‘𝐵)
320 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
321233, 319, 244, 320, 204lmod0vs 20355 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
322317, 318, 321syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
323311, 316, 3223eqtrd 2780 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = (0g𝐵))
324292, 323mpteq2da 5203 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) = (𝑖𝑋 ↦ (0g𝐵)))
325324oveq2d 7373 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))))
326208, 210syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ Abel)
327 ablgrp 19567 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Abel → 𝐵 ∈ Grp)
328 grpmnd 18755 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
329326, 327, 3283syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ Mnd)
330204gsumz 18646 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
331329, 16, 330syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
332331adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
333313adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (0g𝐵) = (0g‘(Scalar‘𝐵)))
334325, 332, 3333eqtrd 2780 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
335334, 142suppss2 8131 . . . . . . . . . . . . . 14 (𝜑 → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
336 suppssfifsupp 9320 . . . . . . . . . . . . . 14 ((((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ V ∧ Fun (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∧ (0g‘(Scalar‘𝐵)) ∈ V) ∧ ({𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin ∧ ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
337203, 252, 253, 283, 335, 336syl32anc 1378 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
338 eqidd 2737 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
339 ovexd 7392 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V)
340338, 339fvmpt2d 6961 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
341340oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
342341mpteq2dva 5205 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
343342oveq2d 7373 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
344119adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
34543ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (.r𝐸) = ( ·𝑠𝐴))
346345oveqd 7374 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
347346mpteq2dva 5205 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))
348118adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
349348oveqd 7374 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
350349mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
351347, 350eqtr3d 2778 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
352351oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
353 eqidd 2737 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝑗 = 𝑗)
354344, 352, 353oveq123d 7378 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
355201oveq1d 7372 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
356354, 355eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
357356mpteq2dva 5205 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
358357oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
35910, 21sraring 32286 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
360162, 36, 359syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ Ring)
361 ringcmn 20003 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
362360, 361syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ CMnd)
363162adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝐸 ∈ Ring)
364 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (LBasis‘𝐵) = (LBasis‘𝐵)
365233, 364lbsss 20538 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
366142, 365syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑌 ⊆ (Base‘𝐵))
367366, 240sseqtrrd 3985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑌 ⊆ (Base‘𝐸))
368367adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑌 ⊆ (Base‘𝐸))
369 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗𝑌)
370368, 369sseldd 3945 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗 ∈ (Base‘𝐸))
37121, 67ringcl 19981 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
372363, 238, 370, 371syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
37337adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (Base‘𝐸) = (Base‘𝐴))
374372, 373eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
375374ralrimivva 3197 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
376 fedgmullem.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
377376fmpo 8000 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378375, 377sylib 217 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
37972, 73, 75, 74, 15, 156, 378, 147lcomf 20361 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
38072, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160lcomfsupp 20362 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) finSupp (0g𝐴))
38174, 134, 362, 142, 16, 379, 380gsumxp 19753 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))))
382 fedgmullem2.2 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (0g𝐴))
3831623ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝐸 ∈ Ring)
3841563ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
38557, 55eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
386385, 36eqsstrrd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
38761, 386eqsstrd 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
388387, 37sseqtrd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
3893883ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390384, 389fssd 6686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
391 simp2 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗𝑌)
392 simp3 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖𝑋)
393390, 391, 392fovcdmd 7526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
394373ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
395393, 394eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
3962383impb 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
3973703impb 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
39821, 67ringass 19984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
399383, 395, 396, 397, 398syl13anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
400399mpoeq3dva 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
401 ovexd 7392 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
402 ovexd 7392 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
403 fnov 7487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
404157, 403sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
405376a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
406142, 16, 401, 402, 404, 405offval22 8020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
40743ofeqd 7619 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
408407oveqd 7374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑊f ( ·𝑠𝐴)𝐷))
409400, 406, 4083eqtr2rd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
410409ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
411410oveqd 7374 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖))
412 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
413 ovexd 7392 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V)
414 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
415414ovmpt4g 7502 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑌𝑖𝑋 ∧ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
416412, 221, 413, 415syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
417411, 416eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
418417mpteq2dva 5205 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) = (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
419418oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))))
420162adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
421367sselda 3944 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
422162ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
423386ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
424423, 219sseldd 3945 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
42521, 67ringcl 19981 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
426422, 424, 239, 425syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
427312adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (0g𝐸) = (0g𝐵))
428245, 350, 4273brtr4d 5137 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
42921, 167, 93, 67, 420, 144, 421, 426, 428gsummulc1 20030 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
430419, 429eqtrd 2776 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
431144mptexd 7174 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) ∈ V)
43215adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝐴 ∈ LMod)
43336adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝑉 ⊆ (Base‘𝐸))
43410, 431, 194, 432, 433gsumsra 31889 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))
435144mptexd 7174 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) ∈ V)
43610, 435, 194, 432, 433gsumsra 31889 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))))
437436oveq1d 7372 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
43843adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐴))
439347oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))))
440438, 439, 353oveq123d 7378 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
441437, 440eqtrd 2776 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
442430, 434, 4413eqtr3d 2784 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
443442mpteq2dva 5205 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)))) = (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)))
444443oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))))
445381, 382, 4443eqtr3rd 2785 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐴))
44610, 1, 9drgext0g 32291 . . . . . . . . . . . . . . . 16 (𝜑 → (0g𝐸) = (0g𝐴))
447445, 446, 3123eqtr2d 2782 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐵))
44810, 1, 9, 11, 2, 142drgextgsum 32296 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
449117, 1, 3, 5, 104, 142drgextgsum 32296 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
450448, 449eqtr3d 2778 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
451358, 447, 4503eqtr3rd 2785 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (0g𝐵))
452343, 451eqtrd 2776 . . . . . . . . . . . . 13 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))
453 breq1 5108 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 finSupp (0g‘(Scalar‘𝐵)) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵))))
454 nfmpt1 5213 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
455454nfeq2 2924 . . . . . . . . . . . . . . . . . . 19 𝑗 𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
456 fveq1 6841 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏𝑗) = ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗))
457456oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
458457adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∧ 𝑗𝑌) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
459455, 458mpteq2da 5203 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)))
460459oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))))
461460eqeq1d 2738 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵) ↔ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)))
462453, 461anbi12d 631 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) ↔ ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))))
463 eqeq1 2740 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
464462, 463imbi12d 344 . . . . . . . . . . . . . 14 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})) ↔ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
465364lbslinds 21239 . . . . . . . . . . . . . . . 16 (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
466465, 142sselid 3942 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (LIndS‘𝐵))
467 eqid 2736 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
468233, 467, 319, 244, 204, 320islinds5 32156 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
469468biimpa 477 . . . . . . . . . . . . . . 15 (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
470208, 366, 466, 469syl21anc 836 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
471 fvexd 6857 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
472 elmapg 8778 . . . . . . . . . . . . . . . 16 (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
473472biimpar 478 . . . . . . . . . . . . . . 15 ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
474471, 142, 251, 473syl21anc 836 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
475464, 470, 474rspcdva 3582 . . . . . . . . . . . . 13 (𝜑 → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
476337, 452, 475mp2and 697 . . . . . . . . . . . 12 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))
477 fconstmpt 5694 . . . . . . . . . . . 12 (𝑌 × {(0g‘(Scalar‘𝐵))}) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵)))
478476, 477eqtrdi 2792 . . . . . . . . . . 11 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))))
479 ovex 7390 . . . . . . . . . . . . 13 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
480479rgenw 3068 . . . . . . . . . . . 12 𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
481 mpteqb 6967 . . . . . . . . . . . 12 (∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵))))
482480, 481ax-mp 5 . . . . . . . . . . 11 ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
483478, 482sylib 217 . . . . . . . . . 10 (𝜑 → ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
484483r19.21bi 3234 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
485312, 446, 3133eqtr3rd 2785 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐴))
486485adantr 481 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g‘(Scalar‘𝐵)) = (0g𝐴))
487202, 484, 4863eqtrd 2780 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))
488183, 487jca 512 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
489186fmpttd 7063 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
490 fvexd 6857 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
491490, 144elmapd 8779 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
492489, 491mpbird 256 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋))
493 simpr 485 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
494493breq1d 5115 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴))))
495 nfv 1917 . . . . . . . . . . . . . 14 𝑖(𝜑𝑗𝑌)
496 nfmpt1 5213 . . . . . . . . . . . . . . 15 𝑖(𝑖𝑋 ↦ (𝑗𝑊𝑖))
497496nfeq2 2924 . . . . . . . . . . . . . 14 𝑖 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
498495, 497nfan 1902 . . . . . . . . . . . . 13 𝑖((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
499 simplr 767 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
500499fveq1d 6844 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → (𝑤𝑖) = ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
501500oveq1d 7372 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → ((𝑤𝑖)( ·𝑠𝐴)𝑖) = (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))
502498, 501mpteq2da 5203 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)))
503502oveq2d 7373 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))))
504503eqeq1d 2738 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴) ↔ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
505494, 504anbi12d 631 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) ↔ ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))))
506493eqeq1d 2738 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))})))
507505, 506imbi12d 344 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) ↔ (((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
508492, 507rspcdv 3573 . . . . . . 7 ((𝜑𝑗𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
509139, 488, 508mp2d 49 . . . . . 6 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
510509, 254eqtrdi 2792 . . . . 5 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
511510, 308sylib 217 . . . 4 ((𝜑𝑗𝑌) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
512511ralrimiva 3143 . . 3 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
513 eqidd 2737 . . . 4 ((𝑗 = 𝑘𝑖 = 𝑙) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴)))
514 fvexd 6857 . . . 4 ((𝜑𝑗𝑌𝑖𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
515 fvexd 6857 . . . 4 ((𝜑𝑘𝑌𝑙𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
516157, 513, 514, 515fnmpoovd 8019 . . 3 (𝜑 → (𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
517512, 516mpbird 256 . 2 (𝜑𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))))
518 fconstmpo 7473 . 2 ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}) = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴)))
519517, 518eqtr4di 2794 1 (𝜑𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  wss 3910  {csn 4586  cop 4592   class class class wbr 5105  cmpt 5188   × cxp 5631  dom cdm 5633  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  f cof 7615   supp csupp 8092  m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  Basecbs 17083  s cress 17112  +gcplusg 17133  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321   Σg cgsu 17322  Mndcmnd 18556  Grpcgrp 18748  SubGrpcsubg 18922  CMndccmn 19562  Abelcabl 19563  Ringcrg 19964  DivRingcdr 20185  SubRingcsubrg 20218  LModclmod 20322  LSubSpclss 20392  LBasisclbs 20535  LVecclvec 20563  subringAlg csra 20629   freeLMod cfrlm 21152  LIndSclinds 21211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-drng 20187  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-lmhm 20483  df-lbs 20536  df-lvec 20564  df-sra 20633  df-rgmod 20634  df-nzr 20728  df-dsmm 21138  df-frlm 21153  df-uvc 21189  df-lindf 21212  df-linds 21213
This theorem is referenced by:  fedgmul  32326
  Copyright terms: Public domain W3C validator