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 33314
Description: Lemma for fedgmul 33315. (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 20530 . . . . . . . . . . . . . 14 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
76biimpa 476 . . . . . . . . . . . . 13 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
83, 4, 7syl2anc 583 . . . . . . . . . . . 12 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
98simpld 494 . . . . . . . . . . 11 (𝜑𝑉 ∈ (SubRing‘𝐸))
10 fedgmul.a . . . . . . . . . . . 12 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11 fedgmul.k . . . . . . . . . . . 12 𝐾 = (𝐸s 𝑉)
1210, 11sralvec 33271 . . . . . . . . . . 11 ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
131, 2, 9, 12syl3anc 1369 . . . . . . . . . 10 (𝜑𝐴 ∈ LVec)
14 lveclmod 20984 . . . . . . . . . 10 (𝐴 ∈ LVec → 𝐴 ∈ LMod)
1513, 14syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ LMod)
16 fedgmullem.x . . . . . . . . . . 11 (𝜑𝑋 ∈ (LBasis‘𝐶))
17 eqid 2727 . . . . . . . . . . . 12 (Base‘𝐶) = (Base‘𝐶)
18 eqid 2727 . . . . . . . . . . . 12 (LBasis‘𝐶) = (LBasis‘𝐶)
1917, 18lbsss 20955 . . . . . . . . . . 11 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
2016, 19syl 17 . . . . . . . . . 10 (𝜑𝑋 ⊆ (Base‘𝐶))
21 eqid 2727 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2221subrgss 20504 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
233, 22syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
245, 21ressbas2 17211 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘𝐹))
26 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
2726a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28 eqid 2727 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
2928subrgss 20504 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
304, 29syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3127, 30srabase 21056 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
3225, 31eqtrd 2767 . . . . . . . . . . . 12 (𝜑𝑈 = (Base‘𝐶))
3332, 23eqsstrrd 4017 . . . . . . . . . . 11 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
3410a1i 11 . . . . . . . . . . . 12 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
3521subrgss 20504 . . . . . . . . . . . . 13 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
369, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑉 ⊆ (Base‘𝐸))
3734, 36srabase 21056 . . . . . . . . . . 11 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
3833, 37sseqtrd 4018 . . . . . . . . . 10 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
3920, 38sstrd 3988 . . . . . . . . 9 (𝜑𝑋 ⊆ (Base‘𝐴))
4034, 3, 36srasubrg 33270 . . . . . . . . . . . 12 (𝜑𝑈 ∈ (SubRing‘𝐴))
41 subrgsubg 20509 . . . . . . . . . . . 12 (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
4240, 41syl 17 . . . . . . . . . . 11 (𝜑𝑈 ∈ (SubGrp‘𝐴))
4310, 1, 9drgextvsca 33276 . . . . . . . . . . . . . 14 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
4443oveqdr 7442 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) = (𝑥( ·𝑠𝐴)𝑦))
453adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
468simprd 495 . . . . . . . . . . . . . . . 16 (𝜑𝑉𝑈)
4746adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉𝑈)
48 simprl 770 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49 ressabs 17223 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
503, 46, 49syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
515oveq1i 7424 . . . . . . . . . . . . . . . . . . . . 21 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
5250, 51, 113eqtr4g 2792 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = 𝐾)
5327, 30srasca 21062 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
5452, 53eqtr3d 2769 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 = (Scalar‘𝐶))
5554fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
5611, 21ressbas2 17211 . . . . . . . . . . . . . . . . . . 19 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
5736, 56syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉 = (Base‘𝐾))
5834, 36srasca 21062 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
5911, 58eqtrid 2779 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 = (Scalar‘𝐴))
6052, 53, 593eqtr3rd 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
6160fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
6255, 57, 613eqtr4d 2777 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 = (Base‘(Scalar‘𝐴)))
6362adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
6448, 63eleqtrrd 2831 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑉)
6547, 64sseldd 3979 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑈)
66 simprr 772 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑦𝑈)
67 eqid 2727 . . . . . . . . . . . . . . 15 (.r𝐸) = (.r𝐸)
6867subrgmcl 20516 . . . . . . . . . . . . . 14 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥𝑈𝑦𝑈) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
6945, 65, 66, 68syl3anc 1369 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
7044, 69eqeltrrd 2829 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
7170ralrimivva 3195 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
72 eqid 2727 . . . . . . . . . . . . 13 (Scalar‘𝐴) = (Scalar‘𝐴)
73 eqid 2727 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74 eqid 2727 . . . . . . . . . . . . 13 (Base‘𝐴) = (Base‘𝐴)
75 eqid 2727 . . . . . . . . . . . . 13 ( ·𝑠𝐴) = ( ·𝑠𝐴)
76 eqid 2727 . . . . . . . . . . . . 13 (LSubSp‘𝐴) = (LSubSp‘𝐴)
7772, 73, 74, 75, 76islss4 20839 . . . . . . . . . . . 12 (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)))
7877biimpar 477 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
7915, 42, 71, 78syl12anc 836 . . . . . . . . . 10 (𝜑𝑈 ∈ (LSubSp‘𝐴))
8020, 32sseqtrrd 4019 . . . . . . . . . 10 (𝜑𝑋𝑈)
8118lbslinds 21760 . . . . . . . . . . . 12 (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
8281, 16sselid 3976 . . . . . . . . . . 11 (𝜑𝑋 ∈ (LIndS‘𝐶))
8323, 37sseqtrd 4018 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐴))
84 eqid 2727 . . . . . . . . . . . . . . 15 (𝐴s 𝑈) = (𝐴s 𝑈)
8584, 74ressbas2 17211 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴s 𝑈)))
8683, 85syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘(𝐴s 𝑈)))
8725, 86, 313eqtr3rd 2776 . . . . . . . . . . . 12 (𝜑 → (Base‘𝐶) = (Base‘(𝐴s 𝑈)))
8884, 72resssca 17317 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
893, 88syl 17 . . . . . . . . . . . . . 14 (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
9060, 89eqtr3d 2769 . . . . . . . . . . . . 13 (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴s 𝑈)))
9190fveq2d 6895 . . . . . . . . . . . 12 (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴s 𝑈))))
9290fveq2d 6895 . . . . . . . . . . . 12 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘(𝐴s 𝑈))))
93 eqid 2727 . . . . . . . . . . . . . . . . 17 (+g𝐸) = (+g𝐸)
945, 93ressplusg 17264 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐸) = (+g𝐹))
953, 94syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐹))
9634, 36sraaddg 21058 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐴))
9727, 30sraaddg 21058 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐹) = (+g𝐶))
9895, 96, 973eqtr3rd 2776 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐶) = (+g𝐴))
99 eqid 2727 . . . . . . . . . . . . . . . 16 (+g𝐴) = (+g𝐴)
10084, 99ressplusg 17264 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐴) = (+g‘(𝐴s 𝑈)))
1013, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐴) = (+g‘(𝐴s 𝑈)))
10298, 101eqtrd 2767 . . . . . . . . . . . . 13 (𝜑 → (+g𝐶) = (+g‘(𝐴s 𝑈)))
103102oveqdr 7442 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g𝐶)𝑦) = (𝑥(+g‘(𝐴s 𝑈))𝑦))
104 fedgmul.2 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ DivRing)
10552, 2eqeltrd 2828 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
106 eqid 2727 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
10726, 106sralvec 33271 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108104, 105, 4, 107syl3anc 1369 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
109 lveclmod 20984 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110108, 109syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
111 eqid 2727 . . . . . . . . . . . . . . 15 (Scalar‘𝐶) = (Scalar‘𝐶)
112 eqid 2727 . . . . . . . . . . . . . . 15 ( ·𝑠𝐶) = ( ·𝑠𝐶)
113 eqid 2727 . . . . . . . . . . . . . . 15 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
11417, 111, 112, 113lmodvscl 20754 . . . . . . . . . . . . . 14 ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
1151143expb 1118 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
116110, 115sylan 579 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
117 fedgmul.b . . . . . . . . . . . . . . . 16 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118117, 1, 3drgextvsca 33276 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
11943, 118eqtr3d 2769 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠𝐵))
12084, 75ressvsca 17318 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1213, 120syl 17 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1225, 67ressmulr 17281 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
1233, 122syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = (.r𝐹))
12426, 104, 4drgextvsca 33276 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
125123, 118, 1243eqtr3d 2775 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐵) = ( ·𝑠𝐶))
126119, 121, 1253eqtr3rd 2776 . . . . . . . . . . . . 13 (𝜑 → ( ·𝑠𝐶) = ( ·𝑠 ‘(𝐴s 𝑈)))
127126oveqdr 7442 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) = (𝑥( ·𝑠 ‘(𝐴s 𝑈))𝑦))
128 ovexd 7449 . . . . . . . . . . . 12 (𝜑 → (𝐴s 𝑈) ∈ V)
12987, 91, 92, 103, 116, 127, 108, 128lindspropd 33092 . . . . . . . . . . 11 (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴s 𝑈)))
13082, 129eleqtrd 2830 . . . . . . . . . 10 (𝜑𝑋 ∈ (LIndS‘(𝐴s 𝑈)))
13176, 84lsslinds 21758 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) → (𝑋 ∈ (LIndS‘(𝐴s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132131biimpa 476 . . . . . . . . . 10 (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
13315, 79, 80, 130, 132syl31anc 1371 . . . . . . . . 9 (𝜑𝑋 ∈ (LIndS‘𝐴))
134 eqid 2727 . . . . . . . . . . 11 (0g𝐴) = (0g𝐴)
135 eqid 2727 . . . . . . . . . . 11 (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
13674, 73, 72, 75, 134, 135islinds5 33073 . . . . . . . . . 10 ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
137136biimpa 476 . . . . . . . . 9 (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
13815, 39, 133, 137syl21anc 837 . . . . . . . 8 (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
139138adantr 480 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
140 eqid 2727 . . . . . . . . . 10 (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
141 fvexd 6906 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (0g𝐹) ∈ V)
142 fedgmullem.y . . . . . . . . . . 11 (𝜑𝑌 ∈ (LBasis‘𝐵))
143142adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑌 ∈ (LBasis‘𝐵))
14416adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145 fedgmullem2.1 . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146 fvexd 6906 . . . . . . . . . . . . . . . 16 (𝜑 → (Scalar‘𝐴) ∈ V)
147142, 16xpexd 7747 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 × 𝑋) ∈ V)
148 eqid 2727 . . . . . . . . . . . . . . . . 17 ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149 eqid 2727 . . . . . . . . . . . . . . . . 17 (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150148, 73, 135, 149frlmelbas 21683 . . . . . . . . . . . . . . . 16 (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
151146, 147, 150syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
152145, 151mpbid 231 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴))))
153152simpld 494 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
154 fvexd 6906 . . . . . . . . . . . . . 14 (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155154, 147elmapd 8852 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156153, 155mpbid 231 . . . . . . . . . . . 12 (𝜑𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157156ffnd 6717 . . . . . . . . . . 11 (𝜑𝑊 Fn (𝑌 × 𝑋))
158157adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159 simpr 484 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑗𝑌)
160152simprd 495 . . . . . . . . . . . 12 (𝜑𝑊 finSupp (0g‘(Scalar‘𝐴)))
161 drngring 20624 . . . . . . . . . . . . . . . 16 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
1621, 161syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ Ring)
163 ringmnd 20176 . . . . . . . . . . . . . . 15 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164162, 163syl 17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ Mnd)
165 subrgsubg 20509 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
1669, 165syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑉 ∈ (SubGrp‘𝐸))
167 eqid 2727 . . . . . . . . . . . . . . . . 17 (0g𝐸) = (0g𝐸)
168167subg0cl 19082 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (SubGrp‘𝐸) → (0g𝐸) ∈ 𝑉)
169166, 168syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0g𝐸) ∈ 𝑉)
17046, 169sseldd 3979 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) ∈ 𝑈)
1715, 21, 167ress0g 18715 . . . . . . . . . . . . . 14 ((𝐸 ∈ Mnd ∧ (0g𝐸) ∈ 𝑈𝑈 ⊆ (Base‘𝐸)) → (0g𝐸) = (0g𝐹))
172164, 170, 23, 171syl3anc 1369 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g𝐹))
17354fveq2d 6895 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
17411, 167subrg0 20511 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
1759, 174syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) = (0g𝐾))
17660fveq2d 6895 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
177173, 175, 1763eqtr4d 2777 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
178172, 177eqtr3d 2769 . . . . . . . . . . . 12 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐴)))
179160, 178breqtrrd 5170 . . . . . . . . . . 11 (𝜑𝑊 finSupp (0g𝐹))
180179adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 finSupp (0g𝐹))
181140, 141, 143, 144, 158, 159, 180fsuppcurry1 32501 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g𝐹))
182178adantr 480 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g𝐹) = (0g‘(Scalar‘𝐴)))
183181, 182breqtrd 5168 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)))
184 eqidd 2728 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
185156fovcdmda 7586 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186185anassrs 467 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187184, 186fvmpt2d 7012 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188187oveq1d 7429 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
189119ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
190189oveqd 7431 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
191188, 190eqtrd 2767 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
192191mpteq2dva 5242 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
193192oveq2d 7430 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1941adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐸 ∈ DivRing)
1959adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑉 ∈ (SubRing‘𝐸))
1962adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐾 ∈ DivRing)
19710, 194, 195, 11, 196, 144drgextgsum 33280 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1983adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199104adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐹 ∈ DivRing)
200117, 194, 198, 5, 199, 144drgextgsum 33280 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
201197, 200eqtr3d 2769 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
202193, 201eqtrd 2767 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
203142mptexd 7230 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ V)
204 eqid 2727 . . . . . . . . . . . . . . . . . 18 (0g𝐵) = (0g𝐵)
205117, 5sralvec 33271 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
2061, 104, 3, 205syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ LVec)
207 lveclmod 20984 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ LMod)
209208adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐵 ∈ LMod)
210 lmodabl 20785 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝐵 ∈ Abel)
212117a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213212, 3, 23srasubrg 33270 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ (SubRing‘𝐵))
214 subrgsubg 20509 . . . . . . . . . . . . . . . . . . . 20 (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215213, 214syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 ∈ (SubGrp‘𝐵))
216215adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217110ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
21861ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219186, 218eleqtrd 2830 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
22020ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
221 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
222220, 221sseldd 3979 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
22317, 111, 112, 113lmodvscl 20754 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
224217, 219, 222, 223syl3anc 1369 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
225125oveqd 7431 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
226225ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
22732ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
228224, 226, 2273eltr4d 2843 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) ∈ 𝑈)
229228fmpttd 7119 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)):𝑋𝑈)
230212, 23srasca 21062 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
2315, 230eqtrid 2779 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 = (Scalar‘𝐵))
232231adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐹 = (Scalar‘𝐵))
233 eqid 2727 . . . . . . . . . . . . . . . . . . 19 (Base‘𝐵) = (Base‘𝐵)
234 ovexd 7449 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
23520, 33sstrd 3988 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ⊆ (Base‘𝐸))
236235adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237 simprr 772 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
238236, 237sseldd 3979 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖 ∈ (Base‘𝐸))
239238anassrs 467 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
240212, 23srabase 21056 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241240ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐵))
242239, 241eleqtrd 2830 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
243 eqid 2727 . . . . . . . . . . . . . . . . . . 19 (0g𝐹) = (0g𝐹)
244 eqid 2727 . . . . . . . . . . . . . . . . . . 19 ( ·𝑠𝐵) = ( ·𝑠𝐵)
245144, 209, 232, 233, 234, 242, 204, 243, 244, 181mptscmfsupp0 20803 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) finSupp (0g𝐵))
246204, 211, 144, 216, 229, 245gsumsubgcl 19868 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ 𝑈)
247231fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
24825, 247eqtrd 2767 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘(Scalar‘𝐵)))
249248adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250246, 249eleqtrd 2830 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251250fmpttd 7119 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252251ffund 6720 . . . . . . . . . . . . . 14 (𝜑 → Fun (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
253 fvexd 6906 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
254 fconstmpt 5734 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × {(0g‘(Scalar‘𝐴))}) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴)))
255254eqeq2i 2740 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
256 ovex 7447 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑊𝑖) ∈ V
257256rgenw 3060 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑋 (𝑘𝑊𝑖) ∈ V
258 mpteqb 7018 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑖𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
259257, 258ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
260255, 259bitri 275 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
261260necon3abii 2982 . . . . . . . . . . . . . . . . . 18 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
262 df-ov 7417 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263262eqcomi 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264263a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265264eqeq1d 2729 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
266265necon3abid 2972 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
267266rexbidva 3171 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
268 rexnal 3095 . . . . . . . . . . . . . . . . . . 19 (∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
269267, 268bitr2di 288 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
270261, 269bitrid 283 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑌) → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
271270rabbidva 3434 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))})
272 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273272neeq1d 2995 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊𝑧) ≠ (0g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
274273dmrab 32288 . . . . . . . . . . . . . . . 16 dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))}
275271, 274eqtr4di 2785 . . . . . . . . . . . . . . 15 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
276 fvexd 6906 . . . . . . . . . . . . . . . . . 18 (𝜑 → (0g‘(Scalar‘𝐴)) ∈ V)
277 suppvalfn 8167 . . . . . . . . . . . . . . . . . 18 ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
278157, 147, 276, 277syl3anc 1369 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
279160fsuppimpd 9387 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) ∈ Fin)
280278, 279eqeltrrd 2829 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
281 dmfi 9348 . . . . . . . . . . . . . . . 16 ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
282280, 281syl 17 . . . . . . . . . . . . . . 15 (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
283275, 282eqeltrd 2828 . . . . . . . . . . . . . 14 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin)
284 nfv 1910 . . . . . . . . . . . . . . . . . . 19 𝑖𝜑
285 nfcv 2898 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑌
286 nfmpt1 5250 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖))
287 nfcv 2898 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑋 × {(0g‘(Scalar‘𝐴))})
288286, 287nfne 3038 . . . . . . . . . . . . . . . . . . . . . 22 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})
289288, 285nfrabw 3463 . . . . . . . . . . . . . . . . . . . . 21 𝑖{𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}
290285, 289nfdif 4121 . . . . . . . . . . . . . . . . . . . 20 𝑖(𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
291290nfcri 2885 . . . . . . . . . . . . . . . . . . 19 𝑖 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
292284, 291nfan 1895 . . . . . . . . . . . . . . . . . 18 𝑖(𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
293 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
294293eldifad 3956 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗𝑌)
295293eldifbd 3957 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
296 oveq1 7421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297296mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑗 → (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
298297neeq1d 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑗 → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
299298elrab 3680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ↔ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
300295, 299sylnib 328 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
301294, 300mpnanrd 409 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}))
302 nne 2939 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
303301, 302sylib 217 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
304303, 254eqtrdi 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
305 ovex 7447 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑊𝑖) ∈ V
306305rgenw 3060 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖𝑋 (𝑗𝑊𝑖) ∈ V
307 mpteqb 7018 . . . . . . . . . . . . . . . . . . . . . . 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 3243 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
311310oveq1d 7429 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖))
312117, 1, 3drgext0g 33275 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐸) = (0g𝐵))
313117, 1, 3drgext0gsca 33277 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐵) = (0g‘(Scalar‘𝐵)))
314312, 177, 3133eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
315314ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
316315oveq1d 7429 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖))
317208ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝐵 ∈ LMod)
318294, 242syldanl 601 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
319 eqid 2727 . . . . . . . . . . . . . . . . . . . . 21 (Scalar‘𝐵) = (Scalar‘𝐵)
320 eqid 2727 . . . . . . . . . . . . . . . . . . . . 21 (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
321233, 319, 244, 320, 204lmod0vs 20771 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
322317, 318, 321syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
323311, 316, 3223eqtrd 2771 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = (0g𝐵))
324292, 323mpteq2da 5240 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) = (𝑖𝑋 ↦ (0g𝐵)))
325324oveq2d 7430 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))))
326208, 210syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ Abel)
327 ablgrp 19733 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Abel → 𝐵 ∈ Grp)
328 grpmnd 18890 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
329326, 327, 3283syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ Mnd)
330204gsumz 18781 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
331329, 16, 330syl2anc 583 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
332331adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
333313adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (0g𝐵) = (0g‘(Scalar‘𝐵)))
334325, 332, 3333eqtrd 2771 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
335334, 142suppss2 8199 . . . . . . . . . . . . . 14 (𝜑 → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
336 suppssfifsupp 9397 . . . . . . . . . . . . . 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 1376 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
338 eqidd 2728 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
339 ovexd 7449 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V)
340338, 339fvmpt2d 7012 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
341340oveq1d 7429 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
342341mpteq2dva 5242 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
343342oveq2d 7430 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
344119adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
34543ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (.r𝐸) = ( ·𝑠𝐴))
346345oveqd 7431 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
347346mpteq2dva 5242 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))
348118adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
349348oveqd 7431 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
350349mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
351347, 350eqtr3d 2769 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
352351oveq2d 7430 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
353 eqidd 2728 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝑗 = 𝑗)
354344, 352, 353oveq123d 7435 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
355201oveq1d 7429 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
356354, 355eqtrd 2767 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
357356mpteq2dva 5242 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
358357oveq2d 7430 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
35910, 21sraring 21072 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
360162, 36, 359syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ Ring)
361 ringcmn 20211 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
362360, 361syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ CMnd)
363162adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝐸 ∈ Ring)
364 eqid 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (LBasis‘𝐵) = (LBasis‘𝐵)
365233, 364lbsss 20955 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
366142, 365syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑌 ⊆ (Base‘𝐵))
367366, 240sseqtrrd 4019 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑌 ⊆ (Base‘𝐸))
368367adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑌 ⊆ (Base‘𝐸))
369 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗𝑌)
370368, 369sseldd 3979 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗 ∈ (Base‘𝐸))
37121, 67ringcl 20183 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
372363, 238, 370, 371syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
37337adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (Base‘𝐸) = (Base‘𝐴))
374372, 373eleqtrd 2830 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
375374ralrimivva 3195 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
376 fedgmullem.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
377376fmpo 8066 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378375, 377sylib 217 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
37972, 73, 75, 74, 15, 156, 378, 147lcomf 20777 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
38072, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160lcomfsupp 20778 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) finSupp (0g𝐴))
38174, 134, 362, 142, 16, 379, 380gsumxp 19924 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))))
382 fedgmullem2.2 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (0g𝐴))
3831623ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝐸 ∈ Ring)
3841563ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
38557, 55eqtrd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
386385, 36eqsstrrd 4017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
38761, 386eqsstrd 4016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
388387, 37sseqtrd 4018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
3893883ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390384, 389fssd 6734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
391 simp2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗𝑌)
392 simp3 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖𝑋)
393390, 391, 392fovcdmd 7587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
394373ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
395393, 394eleqtrrd 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
3962383impb 1113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
3973703impb 1113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
39821, 67ringass 20186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
399383, 395, 396, 397, 398syl13anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
400399mpoeq3dva 7491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
401 ovexd 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
402 ovexd 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
403 fnov 7546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
404157, 403sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
405376a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
406142, 16, 401, 402, 404, 405offval22 8087 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
40743ofeqd 7681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
408407oveqd 7431 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑊f ( ·𝑠𝐴)𝐷))
409400, 406, 4083eqtr2rd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
410409ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
411410oveqd 7431 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖))
412 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
413 ovexd 7449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V)
414 eqid 2727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
415414ovmpt4g 7562 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑌𝑖𝑋 ∧ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
416412, 221, 413, 415syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
417411, 416eqtrd 2767 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
418417mpteq2dva 5242 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) = (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
419418oveq2d 7430 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))))
420162adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
421367sselda 3978 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
422162ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
423386ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
424423, 219sseldd 3979 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
42521, 67ringcl 20183 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
426422, 424, 239, 425syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
427312adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (0g𝐸) = (0g𝐵))
428245, 350, 4273brtr4d 5174 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
42921, 167, 67, 420, 144, 421, 426, 428gsummulc1 20245 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
430419, 429eqtrd 2767 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
431144mptexd 7230 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) ∈ V)
43215adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝐴 ∈ LMod)
43336adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝑉 ⊆ (Base‘𝐸))
43410, 431, 194, 432, 433gsumsra 32755 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))
435144mptexd 7230 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) ∈ V)
43610, 435, 194, 432, 433gsumsra 32755 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))))
437436oveq1d 7429 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
43843adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐴))
439347oveq2d 7430 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))))
440438, 439, 353oveq123d 7435 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
441437, 440eqtrd 2767 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
442430, 434, 4413eqtr3d 2775 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
443442mpteq2dva 5242 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)))) = (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)))
444443oveq2d 7430 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))))
445381, 382, 4443eqtr3rd 2776 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐴))
44610, 1, 9drgext0g 33275 . . . . . . . . . . . . . . . 16 (𝜑 → (0g𝐸) = (0g𝐴))
447445, 446, 3123eqtr2d 2773 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐵))
44810, 1, 9, 11, 2, 142drgextgsum 33280 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
449117, 1, 3, 5, 104, 142drgextgsum 33280 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
450448, 449eqtr3d 2769 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
451358, 447, 4503eqtr3rd 2776 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (0g𝐵))
452343, 451eqtrd 2767 . . . . . . . . . . . . 13 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))
453 breq1 5145 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 finSupp (0g‘(Scalar‘𝐵)) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵))))
454 nfmpt1 5250 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
455454nfeq2 2915 . . . . . . . . . . . . . . . . . . 19 𝑗 𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
456 fveq1 6890 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏𝑗) = ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗))
457456oveq1d 7429 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
458457adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∧ 𝑗𝑌) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
459455, 458mpteq2da 5240 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)))
460459oveq2d 7430 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))))
461460eqeq1d 2729 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵) ↔ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)))
462453, 461anbi12d 630 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) ↔ ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))))
463 eqeq1 2731 . . . . . . . . . . . . . . 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 21760 . . . . . . . . . . . . . . . 16 (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
466465, 142sselid 3976 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (LIndS‘𝐵))
467 eqid 2727 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
468233, 467, 319, 244, 204, 320islinds5 33073 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
469468biimpa 476 . . . . . . . . . . . . . . 15 (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
470208, 366, 466, 469syl21anc 837 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
471 fvexd 6906 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
472 elmapg 8851 . . . . . . . . . . . . . . . 16 (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
473472biimpar 477 . . . . . . . . . . . . . . 15 ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
474471, 142, 251, 473syl21anc 837 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
475464, 470, 474rspcdva 3608 . . . . . . . . . . . . 13 (𝜑 → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
476337, 452, 475mp2and 698 . . . . . . . . . . . 12 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))
477 fconstmpt 5734 . . . . . . . . . . . 12 (𝑌 × {(0g‘(Scalar‘𝐵))}) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵)))
478476, 477eqtrdi 2783 . . . . . . . . . . 11 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))))
479 ovex 7447 . . . . . . . . . . . . 13 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
480479rgenw 3060 . . . . . . . . . . . 12 𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
481 mpteqb 7018 . . . . . . . . . . . 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 3243 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
485312, 446, 3133eqtr3rd 2776 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐴))
486485adantr 480 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g‘(Scalar‘𝐵)) = (0g𝐴))
487202, 484, 4863eqtrd 2771 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))
488183, 487jca 511 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
489186fmpttd 7119 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
490 fvexd 6906 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
491490, 144elmapd 8852 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
492489, 491mpbird 257 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋))
493 simpr 484 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
494493breq1d 5152 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴))))
495 nfv 1910 . . . . . . . . . . . . . 14 𝑖(𝜑𝑗𝑌)
496 nfmpt1 5250 . . . . . . . . . . . . . . 15 𝑖(𝑖𝑋 ↦ (𝑗𝑊𝑖))
497496nfeq2 2915 . . . . . . . . . . . . . 14 𝑖 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
498495, 497nfan 1895 . . . . . . . . . . . . 13 𝑖((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
499 simplr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
500499fveq1d 6893 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → (𝑤𝑖) = ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
501500oveq1d 7429 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → ((𝑤𝑖)( ·𝑠𝐴)𝑖) = (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))
502498, 501mpteq2da 5240 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)))
503502oveq2d 7430 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))))
504503eqeq1d 2729 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴) ↔ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
505494, 504anbi12d 630 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) ↔ ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))))
506493eqeq1d 2729 . . . . . . . . 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 3599 . . . . . . 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 2783 . . . . 5 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
511510, 308sylib 217 . . . 4 ((𝜑𝑗𝑌) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
512511ralrimiva 3141 . . 3 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
513 eqidd 2728 . . . 4 ((𝑗 = 𝑘𝑖 = 𝑙) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴)))
514 fvexd 6906 . . . 4 ((𝜑𝑗𝑌𝑖𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
515 fvexd 6906 . . . 4 ((𝜑𝑘𝑌𝑙𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
516157, 513, 514, 515fnmpoovd 8086 . . 3 (𝜑 → (𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
517512, 516mpbird 257 . 2 (𝜑𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))))
518 fconstmpo 7531 . 2 ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}) = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴)))
519517, 518eqtr4di 2785 1 (𝜑𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2935  wral 3056  wrex 3065  {crab 3427  Vcvv 3469  cdif 3941  wss 3944  {csn 4624  cop 4630   class class class wbr 5142  cmpt 5225   × cxp 5670  dom cdm 5672  Fun wfun 6536   Fn wfn 6537  wf 6538  cfv 6542  (class class class)co 7414  cmpo 7416  f cof 7677   supp csupp 8159  m cmap 8838  Fincfn 8957   finSupp cfsupp 9379  Basecbs 17173  s cress 17202  +gcplusg 17226  .rcmulr 17227  Scalarcsca 17229   ·𝑠 cvsca 17230  0gc0g 17414   Σg cgsu 17415  Mndcmnd 18687  Grpcgrp 18883  SubGrpcsubg 19068  CMndccmn 19728  Abelcabl 19729  Ringcrg 20166  SubRingcsubrg 20499  DivRingcdr 20617  LModclmod 20736  LSubSpclss 20808  LBasisclbs 20952  LVecclvec 20980  subringAlg csra 21049   freeLMod cfrlm 21673  LIndSclinds 21732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8840  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9380  df-sup 9459  df-oi 9527  df-card 9956  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-nn 12237  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305  df-9 12306  df-n0 12497  df-z 12583  df-dec 12702  df-uz 12847  df-fz 13511  df-fzo 13654  df-seq 13993  df-hash 14316  df-struct 17109  df-sets 17126  df-slot 17144  df-ndx 17156  df-base 17174  df-ress 17203  df-plusg 17239  df-mulr 17240  df-sca 17242  df-vsca 17243  df-ip 17244  df-tset 17245  df-ple 17246  df-ds 17248  df-hom 17250  df-cco 17251  df-0g 17416  df-gsum 17417  df-prds 17422  df-pws 17424  df-mre 17559  df-mrc 17560  df-acs 17562  df-mgm 18593  df-sgrp 18672  df-mnd 18688  df-mhm 18733  df-submnd 18734  df-grp 18886  df-minusg 18887  df-sbg 18888  df-mulg 19017  df-subg 19071  df-ghm 19161  df-cntz 19261  df-cmn 19730  df-abl 19731  df-mgp 20068  df-rng 20086  df-ur 20115  df-ring 20168  df-nzr 20445  df-subrng 20476  df-subrg 20501  df-drng 20619  df-lmod 20738  df-lss 20809  df-lsp 20849  df-lmhm 20900  df-lbs 20953  df-lvec 20981  df-sra 21051  df-rgmod 21052  df-dsmm 21659  df-frlm 21674  df-uvc 21710  df-lindf 21733  df-linds 21734
This theorem is referenced by:  fedgmul  33315
  Copyright terms: Public domain W3C validator