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 33657
Description: Lemma for fedgmul 33658. (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 20614 . . . . . . . . . . . . . 14 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
76biimpa 476 . . . . . . . . . . . . 13 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
83, 4, 7syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
98simpld 494 . . . . . . . . . . 11 (𝜑𝑉 ∈ (SubRing‘𝐸))
10 fedgmul.a . . . . . . . . . . . 12 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11 fedgmul.k . . . . . . . . . . . 12 𝐾 = (𝐸s 𝑉)
1210, 11sralvec 33614 . . . . . . . . . . 11 ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
131, 2, 9, 12syl3anc 1370 . . . . . . . . . 10 (𝜑𝐴 ∈ LVec)
14 lveclmod 21122 . . . . . . . . . 10 (𝐴 ∈ LVec → 𝐴 ∈ LMod)
1513, 14syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ LMod)
16 fedgmullem.x . . . . . . . . . . 11 (𝜑𝑋 ∈ (LBasis‘𝐶))
17 eqid 2734 . . . . . . . . . . . 12 (Base‘𝐶) = (Base‘𝐶)
18 eqid 2734 . . . . . . . . . . . 12 (LBasis‘𝐶) = (LBasis‘𝐶)
1917, 18lbsss 21093 . . . . . . . . . . 11 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
2016, 19syl 17 . . . . . . . . . 10 (𝜑𝑋 ⊆ (Base‘𝐶))
21 eqid 2734 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2221subrgss 20588 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
233, 22syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
245, 21ressbas2 17282 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘𝐹))
26 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
2726a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28 eqid 2734 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
2928subrgss 20588 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
304, 29syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3127, 30srabase 21194 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
3225, 31eqtrd 2774 . . . . . . . . . . . 12 (𝜑𝑈 = (Base‘𝐶))
3332, 23eqsstrrd 4034 . . . . . . . . . . 11 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
3410a1i 11 . . . . . . . . . . . 12 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
3521subrgss 20588 . . . . . . . . . . . . 13 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
369, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑉 ⊆ (Base‘𝐸))
3734, 36srabase 21194 . . . . . . . . . . 11 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
3833, 37sseqtrd 4035 . . . . . . . . . 10 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
3920, 38sstrd 4005 . . . . . . . . 9 (𝜑𝑋 ⊆ (Base‘𝐴))
4034, 3, 36srasubrg 33613 . . . . . . . . . . . 12 (𝜑𝑈 ∈ (SubRing‘𝐴))
41 subrgsubg 20593 . . . . . . . . . . . 12 (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
4240, 41syl 17 . . . . . . . . . . 11 (𝜑𝑈 ∈ (SubGrp‘𝐴))
4310, 1, 9drgextvsca 33619 . . . . . . . . . . . . . 14 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
4443oveqdr 7458 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) = (𝑥( ·𝑠𝐴)𝑦))
453adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
468simprd 495 . . . . . . . . . . . . . . . 16 (𝜑𝑉𝑈)
4746adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉𝑈)
48 simprl 771 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49 ressabs 17294 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
503, 46, 49syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
515oveq1i 7440 . . . . . . . . . . . . . . . . . . . . 21 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
5250, 51, 113eqtr4g 2799 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = 𝐾)
5327, 30srasca 21200 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
5452, 53eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 = (Scalar‘𝐶))
5554fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
5611, 21ressbas2 17282 . . . . . . . . . . . . . . . . . . 19 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
5736, 56syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉 = (Base‘𝐾))
5834, 36srasca 21200 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
5911, 58eqtrid 2786 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 = (Scalar‘𝐴))
6052, 53, 593eqtr3rd 2783 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
6160fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
6255, 57, 613eqtr4d 2784 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 = (Base‘(Scalar‘𝐴)))
6362adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
6448, 63eleqtrrd 2841 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑉)
6547, 64sseldd 3995 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑈)
66 simprr 773 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑦𝑈)
67 eqid 2734 . . . . . . . . . . . . . . 15 (.r𝐸) = (.r𝐸)
6867subrgmcl 20600 . . . . . . . . . . . . . 14 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥𝑈𝑦𝑈) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
6945, 65, 66, 68syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
7044, 69eqeltrrd 2839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
7170ralrimivva 3199 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
72 eqid 2734 . . . . . . . . . . . . 13 (Scalar‘𝐴) = (Scalar‘𝐴)
73 eqid 2734 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74 eqid 2734 . . . . . . . . . . . . 13 (Base‘𝐴) = (Base‘𝐴)
75 eqid 2734 . . . . . . . . . . . . 13 ( ·𝑠𝐴) = ( ·𝑠𝐴)
76 eqid 2734 . . . . . . . . . . . . 13 (LSubSp‘𝐴) = (LSubSp‘𝐴)
7772, 73, 74, 75, 76islss4 20977 . . . . . . . . . . . 12 (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)))
7877biimpar 477 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
7915, 42, 71, 78syl12anc 837 . . . . . . . . . 10 (𝜑𝑈 ∈ (LSubSp‘𝐴))
8020, 32sseqtrrd 4036 . . . . . . . . . 10 (𝜑𝑋𝑈)
8118lbslinds 21870 . . . . . . . . . . . 12 (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
8281, 16sselid 3992 . . . . . . . . . . 11 (𝜑𝑋 ∈ (LIndS‘𝐶))
8323, 37sseqtrd 4035 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐴))
84 eqid 2734 . . . . . . . . . . . . . . 15 (𝐴s 𝑈) = (𝐴s 𝑈)
8584, 74ressbas2 17282 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴s 𝑈)))
8683, 85syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘(𝐴s 𝑈)))
8725, 86, 313eqtr3rd 2783 . . . . . . . . . . . 12 (𝜑 → (Base‘𝐶) = (Base‘(𝐴s 𝑈)))
8884, 72resssca 17388 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
893, 88syl 17 . . . . . . . . . . . . . 14 (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
9060, 89eqtr3d 2776 . . . . . . . . . . . . 13 (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴s 𝑈)))
9190fveq2d 6910 . . . . . . . . . . . 12 (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴s 𝑈))))
9290fveq2d 6910 . . . . . . . . . . . 12 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘(𝐴s 𝑈))))
93 eqid 2734 . . . . . . . . . . . . . . . . 17 (+g𝐸) = (+g𝐸)
945, 93ressplusg 17335 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐸) = (+g𝐹))
953, 94syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐹))
9634, 36sraaddg 21196 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐴))
9727, 30sraaddg 21196 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐹) = (+g𝐶))
9895, 96, 973eqtr3rd 2783 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐶) = (+g𝐴))
99 eqid 2734 . . . . . . . . . . . . . . . 16 (+g𝐴) = (+g𝐴)
10084, 99ressplusg 17335 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐴) = (+g‘(𝐴s 𝑈)))
1013, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐴) = (+g‘(𝐴s 𝑈)))
10298, 101eqtrd 2774 . . . . . . . . . . . . 13 (𝜑 → (+g𝐶) = (+g‘(𝐴s 𝑈)))
103102oveqdr 7458 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g𝐶)𝑦) = (𝑥(+g‘(𝐴s 𝑈))𝑦))
104 fedgmul.2 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ DivRing)
10552, 2eqeltrd 2838 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
106 eqid 2734 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
10726, 106sralvec 33614 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108104, 105, 4, 107syl3anc 1370 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
109 lveclmod 21122 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110108, 109syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
111 eqid 2734 . . . . . . . . . . . . . . 15 (Scalar‘𝐶) = (Scalar‘𝐶)
112 eqid 2734 . . . . . . . . . . . . . . 15 ( ·𝑠𝐶) = ( ·𝑠𝐶)
113 eqid 2734 . . . . . . . . . . . . . . 15 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
11417, 111, 112, 113lmodvscl 20892 . . . . . . . . . . . . . 14 ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
1151143expb 1119 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
116110, 115sylan 580 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
117 fedgmul.b . . . . . . . . . . . . . . . 16 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118117, 1, 3drgextvsca 33619 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
11943, 118eqtr3d 2776 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠𝐵))
12084, 75ressvsca 17389 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1213, 120syl 17 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1225, 67ressmulr 17352 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
1233, 122syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = (.r𝐹))
12426, 104, 4drgextvsca 33619 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
125123, 118, 1243eqtr3d 2782 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐵) = ( ·𝑠𝐶))
126119, 121, 1253eqtr3rd 2783 . . . . . . . . . . . . 13 (𝜑 → ( ·𝑠𝐶) = ( ·𝑠 ‘(𝐴s 𝑈)))
127126oveqdr 7458 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) = (𝑥( ·𝑠 ‘(𝐴s 𝑈))𝑦))
128 ovexd 7465 . . . . . . . . . . . 12 (𝜑 → (𝐴s 𝑈) ∈ V)
12987, 91, 92, 103, 116, 127, 108, 128lindspropd 33390 . . . . . . . . . . 11 (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴s 𝑈)))
13082, 129eleqtrd 2840 . . . . . . . . . 10 (𝜑𝑋 ∈ (LIndS‘(𝐴s 𝑈)))
13176, 84lsslinds 21868 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) → (𝑋 ∈ (LIndS‘(𝐴s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132131biimpa 476 . . . . . . . . . 10 (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
13315, 79, 80, 130, 132syl31anc 1372 . . . . . . . . 9 (𝜑𝑋 ∈ (LIndS‘𝐴))
134 eqid 2734 . . . . . . . . . . 11 (0g𝐴) = (0g𝐴)
135 eqid 2734 . . . . . . . . . . 11 (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
13674, 73, 72, 75, 134, 135islinds5 33374 . . . . . . . . . 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 838 . . . . . . . 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 2734 . . . . . . . . . 10 (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
141 fvexd 6921 . . . . . . . . . 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 6921 . . . . . . . . . . . . . . . 16 (𝜑 → (Scalar‘𝐴) ∈ V)
147142, 16xpexd 7769 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 × 𝑋) ∈ V)
148 eqid 2734 . . . . . . . . . . . . . . . . 17 ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149 eqid 2734 . . . . . . . . . . . . . . . . 17 (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150148, 73, 135, 149frlmelbas 21793 . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴))))
153152simpld 494 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
154 fvexd 6921 . . . . . . . . . . . . . 14 (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155154, 147elmapd 8878 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156153, 155mpbid 232 . . . . . . . . . . . 12 (𝜑𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157156ffnd 6737 . . . . . . . . . . 11 (𝜑𝑊 Fn (𝑌 × 𝑋))
158157adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159 simpr 484 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑗𝑌)
160152simprd 495 . . . . . . . . . . . 12 (𝜑𝑊 finSupp (0g‘(Scalar‘𝐴)))
161 drngring 20752 . . . . . . . . . . . . . . . 16 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
1621, 161syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ Ring)
163 ringmnd 20260 . . . . . . . . . . . . . . 15 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164162, 163syl 17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ Mnd)
165 subrgsubg 20593 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
1669, 165syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑉 ∈ (SubGrp‘𝐸))
167 eqid 2734 . . . . . . . . . . . . . . . . 17 (0g𝐸) = (0g𝐸)
168167subg0cl 19164 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (SubGrp‘𝐸) → (0g𝐸) ∈ 𝑉)
169166, 168syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0g𝐸) ∈ 𝑉)
17046, 169sseldd 3995 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) ∈ 𝑈)
1715, 21, 167ress0g 18787 . . . . . . . . . . . . . 14 ((𝐸 ∈ Mnd ∧ (0g𝐸) ∈ 𝑈𝑈 ⊆ (Base‘𝐸)) → (0g𝐸) = (0g𝐹))
172164, 170, 23, 171syl3anc 1370 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g𝐹))
17354fveq2d 6910 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
17411, 167subrg0 20595 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
1759, 174syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) = (0g𝐾))
17660fveq2d 6910 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
177173, 175, 1763eqtr4d 2784 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
178172, 177eqtr3d 2776 . . . . . . . . . . . 12 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐴)))
179160, 178breqtrrd 5175 . . . . . . . . . . 11 (𝜑𝑊 finSupp (0g𝐹))
180179adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 finSupp (0g𝐹))
181140, 141, 143, 144, 158, 159, 180fsuppcurry1 32742 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g𝐹))
182178adantr 480 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g𝐹) = (0g‘(Scalar‘𝐴)))
183181, 182breqtrd 5173 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)))
184 eqidd 2735 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
185156fovcdmda 7603 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186185anassrs 467 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187184, 186fvmpt2d 7028 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188187oveq1d 7445 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
189119ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
190189oveqd 7447 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
191188, 190eqtrd 2774 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
192191mpteq2dva 5247 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
193192oveq2d 7446 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1941adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐸 ∈ DivRing)
1959adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑉 ∈ (SubRing‘𝐸))
1962adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐾 ∈ DivRing)
19710, 194, 195, 11, 196, 144drgextgsum 33623 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1983adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199104adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐹 ∈ DivRing)
200117, 194, 198, 5, 199, 144drgextgsum 33623 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
201197, 200eqtr3d 2776 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
202193, 201eqtrd 2774 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
203142mptexd 7243 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ V)
204 eqid 2734 . . . . . . . . . . . . . . . . . 18 (0g𝐵) = (0g𝐵)
205117, 5sralvec 33614 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
2061, 104, 3, 205syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ LVec)
207 lveclmod 21122 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ LMod)
209208adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐵 ∈ LMod)
210 lmodabl 20923 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝐵 ∈ Abel)
212117a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213212, 3, 23srasubrg 33613 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ (SubRing‘𝐵))
214 subrgsubg 20593 . . . . . . . . . . . . . . . . . . . 20 (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215213, 214syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 ∈ (SubGrp‘𝐵))
216215adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217110ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
21861ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219186, 218eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
22020ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
221 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
222220, 221sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
22317, 111, 112, 113lmodvscl 20892 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
224217, 219, 222, 223syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
225125oveqd 7447 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
226225ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
22732ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
228224, 226, 2273eltr4d 2853 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) ∈ 𝑈)
229228fmpttd 7134 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)):𝑋𝑈)
230212, 23srasca 21200 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
2315, 230eqtrid 2786 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 = (Scalar‘𝐵))
232231adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐹 = (Scalar‘𝐵))
233 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (Base‘𝐵) = (Base‘𝐵)
234 ovexd 7465 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
23520, 33sstrd 4005 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ⊆ (Base‘𝐸))
236235adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237 simprr 773 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
238236, 237sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖 ∈ (Base‘𝐸))
239238anassrs 467 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
240212, 23srabase 21194 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241240ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐵))
242239, 241eleqtrd 2840 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
243 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (0g𝐹) = (0g𝐹)
244 eqid 2734 . . . . . . . . . . . . . . . . . . 19 ( ·𝑠𝐵) = ( ·𝑠𝐵)
245144, 209, 232, 233, 234, 242, 204, 243, 244, 181mptscmfsupp0 20941 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) finSupp (0g𝐵))
246204, 211, 144, 216, 229, 245gsumsubgcl 19952 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ 𝑈)
247231fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
24825, 247eqtrd 2774 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘(Scalar‘𝐵)))
249248adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250246, 249eleqtrd 2840 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251250fmpttd 7134 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252251ffund 6740 . . . . . . . . . . . . . 14 (𝜑 → Fun (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
253 fvexd 6921 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
254 fconstmpt 5750 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × {(0g‘(Scalar‘𝐴))}) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴)))
255254eqeq2i 2747 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
256 ovex 7463 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑊𝑖) ∈ V
257256rgenw 3062 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑋 (𝑘𝑊𝑖) ∈ V
258 mpteqb 7034 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑖𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
259257, 258ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
260255, 259bitri 275 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
261260necon3abii 2984 . . . . . . . . . . . . . . . . . 18 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
262 df-ov 7433 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263262eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264263a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265264eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
266265necon3abid 2974 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
267266rexbidva 3174 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
268 rexnal 3097 . . . . . . . . . . . . . . . . . . 19 (∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
269267, 268bitr2di 288 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
270261, 269bitrid 283 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑌) → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
271270rabbidva 3439 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))})
272 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273272neeq1d 2997 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊𝑧) ≠ (0g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
274273dmrab 32524 . . . . . . . . . . . . . . . 16 dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))}
275271, 274eqtr4di 2792 . . . . . . . . . . . . . . 15 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
276 fvexd 6921 . . . . . . . . . . . . . . . . . 18 (𝜑 → (0g‘(Scalar‘𝐴)) ∈ V)
277 suppvalfn 8191 . . . . . . . . . . . . . . . . . 18 ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
278157, 147, 276, 277syl3anc 1370 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
279160fsuppimpd 9406 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) ∈ Fin)
280278, 279eqeltrrd 2839 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
281 dmfi 9372 . . . . . . . . . . . . . . . 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 1911 . . . . . . . . . . . . . . . . . . 19 𝑖𝜑
285 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑌
286 nfmpt1 5255 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖))
287 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑋 × {(0g‘(Scalar‘𝐴))})
288286, 287nfne 3040 . . . . . . . . . . . . . . . . . . . . . 22 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})
289288, 285nfrabw 3472 . . . . . . . . . . . . . . . . . . . . 21 𝑖{𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}
290285, 289nfdif 4138 . . . . . . . . . . . . . . . . . . . 20 𝑖(𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
291290nfcri 2894 . . . . . . . . . . . . . . . . . . 19 𝑖 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
292284, 291nfan 1896 . . . . . . . . . . . . . . . . . 18 𝑖(𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
293 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
294293eldifad 3974 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗𝑌)
295293eldifbd 3975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
296 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297296mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑗 → (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
298297neeq1d 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑗 → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
299298elrab 3694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ↔ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
300295, 299sylnib 328 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
301294, 300mpnanrd 409 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}))
302 nne 2941 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
303301, 302sylib 218 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
304303, 254eqtrdi 2790 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
305 ovex 7463 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑊𝑖) ∈ V
306305rgenw 3062 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖𝑋 (𝑗𝑊𝑖) ∈ V
307 mpteqb 7034 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
308306, 307ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
309304, 308sylib 218 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
310309r19.21bi 3248 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
311310oveq1d 7445 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖))
312117, 1, 3drgext0g 33618 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐸) = (0g𝐵))
313117, 1, 3drgext0gsca 33620 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐵) = (0g‘(Scalar‘𝐵)))
314312, 177, 3133eqtr3d 2782 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
315314ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
316315oveq1d 7445 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖))
317208ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝐵 ∈ LMod)
318294, 242syldanl 602 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
319 eqid 2734 . . . . . . . . . . . . . . . . . . . . 21 (Scalar‘𝐵) = (Scalar‘𝐵)
320 eqid 2734 . . . . . . . . . . . . . . . . . . . . 21 (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
321233, 319, 244, 320, 204lmod0vs 20909 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
322317, 318, 321syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
323311, 316, 3223eqtrd 2778 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = (0g𝐵))
324292, 323mpteq2da 5245 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) = (𝑖𝑋 ↦ (0g𝐵)))
325324oveq2d 7446 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))))
326 ablgrp 19817 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Abel → 𝐵 ∈ Grp)
327 grpmnd 18970 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
328208, 210, 326, 3274syl 19 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ Mnd)
329204gsumz 18861 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
330328, 16, 329syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
331330adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
332313adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (0g𝐵) = (0g‘(Scalar‘𝐵)))
333325, 331, 3323eqtrd 2778 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
334333, 142suppss2 8223 . . . . . . . . . . . . . 14 (𝜑 → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
335 suppssfifsupp 9417 . . . . . . . . . . . . . 14 ((((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ V ∧ Fun (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∧ (0g‘(Scalar‘𝐵)) ∈ V) ∧ ({𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin ∧ ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
336203, 252, 253, 283, 334, 335syl32anc 1377 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
337 eqidd 2735 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
338 ovexd 7465 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V)
339337, 338fvmpt2d 7028 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
340339oveq1d 7445 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
341340mpteq2dva 5247 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
342341oveq2d 7446 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
343119adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
34443ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (.r𝐸) = ( ·𝑠𝐴))
345344oveqd 7447 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
346345mpteq2dva 5247 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))
347118adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
348347oveqd 7447 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
349348mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
350346, 349eqtr3d 2776 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
351350oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
352 eqidd 2735 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝑗 = 𝑗)
353343, 351, 352oveq123d 7451 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
354201oveq1d 7445 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
355353, 354eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
356355mpteq2dva 5247 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
357356oveq2d 7446 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
35810, 21sraring 21210 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
359162, 36, 358syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ Ring)
360 ringcmn 20295 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
361359, 360syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ CMnd)
362162adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝐸 ∈ Ring)
363 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (LBasis‘𝐵) = (LBasis‘𝐵)
364233, 363lbsss 21093 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
365142, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑌 ⊆ (Base‘𝐵))
366365, 240sseqtrrd 4036 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑌 ⊆ (Base‘𝐸))
367366adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑌 ⊆ (Base‘𝐸))
368 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗𝑌)
369367, 368sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗 ∈ (Base‘𝐸))
37021, 67ringcl 20267 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
371362, 238, 369, 370syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
37237adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (Base‘𝐸) = (Base‘𝐴))
373371, 372eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
374373ralrimivva 3199 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
375 fedgmullem.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
376375fmpo 8091 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
377374, 376sylib 218 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
37872, 73, 75, 74, 15, 156, 377, 147lcomf 20915 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
37972, 73, 75, 74, 15, 156, 377, 147, 134, 135, 160lcomfsupp 20916 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) finSupp (0g𝐴))
38074, 134, 361, 142, 16, 378, 379gsumxp 20008 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))))
381 fedgmullem2.2 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (0g𝐴))
3821623ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝐸 ∈ Ring)
3831563ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
38457, 55eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
385384, 36eqsstrrd 4034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
38661, 385eqsstrd 4033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
387386, 37sseqtrd 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
3883873ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389383, 388fssd 6753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
390 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗𝑌)
391 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖𝑋)
392389, 390, 391fovcdmd 7604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
393373ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
394392, 393eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
3952383impb 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
3963693impb 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
39721, 67ringass 20270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
398382, 394, 395, 396, 397syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
399398mpoeq3dva 7509 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
400 ovexd 7465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
401 ovexd 7465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
402 fnov 7563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
403157, 402sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
404375a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
405142, 16, 400, 401, 403, 404offval22 8111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
40643ofeqd 7698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
407406oveqd 7447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑊f ( ·𝑠𝐴)𝐷))
408399, 405, 4073eqtr2rd 2781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
409408ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
410409oveqd 7447 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖))
411 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
412 ovexd 7465 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V)
413 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
414413ovmpt4g 7579 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑌𝑖𝑋 ∧ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
415411, 221, 412, 414syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
416410, 415eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
417416mpteq2dva 5247 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) = (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
418417oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))))
419162adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
420366sselda 3994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
421162ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
422385ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
423422, 219sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
42421, 67ringcl 20267 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
425421, 423, 239, 424syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
426312adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (0g𝐸) = (0g𝐵))
427245, 349, 4263brtr4d 5179 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
42821, 167, 67, 419, 144, 420, 425, 427gsummulc1 20329 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
429418, 428eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
430144mptexd 7243 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) ∈ V)
43115adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝐴 ∈ LMod)
43236adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝑉 ⊆ (Base‘𝐸))
43310, 430, 194, 431, 432gsumsra 33032 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))
434144mptexd 7243 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) ∈ V)
43510, 434, 194, 431, 432gsumsra 33032 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))))
436435oveq1d 7445 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
43743adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐴))
438346oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))))
439437, 438, 352oveq123d 7451 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
440436, 439eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
441429, 433, 4403eqtr3d 2782 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
442441mpteq2dva 5247 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)))) = (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)))
443442oveq2d 7446 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))))
444380, 381, 4433eqtr3rd 2783 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐴))
44510, 1, 9drgext0g 33618 . . . . . . . . . . . . . . . 16 (𝜑 → (0g𝐸) = (0g𝐴))
446444, 445, 3123eqtr2d 2780 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐵))
44710, 1, 9, 11, 2, 142drgextgsum 33623 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
448117, 1, 3, 5, 104, 142drgextgsum 33623 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
449447, 448eqtr3d 2776 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
450357, 446, 4493eqtr3rd 2783 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (0g𝐵))
451342, 450eqtrd 2774 . . . . . . . . . . . . 13 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))
452 breq1 5150 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 finSupp (0g‘(Scalar‘𝐵)) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵))))
453 nfmpt1 5255 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
454453nfeq2 2920 . . . . . . . . . . . . . . . . . . 19 𝑗 𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
455 fveq1 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏𝑗) = ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗))
456455oveq1d 7445 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
457456adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∧ 𝑗𝑌) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
458454, 457mpteq2da 5245 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)))
459458oveq2d 7446 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))))
460459eqeq1d 2736 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵) ↔ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)))
461452, 460anbi12d 632 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) ↔ ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))))
462 eqeq1 2738 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
463461, 462imbi12d 344 . . . . . . . . . . . . . 14 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})) ↔ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
464363lbslinds 21870 . . . . . . . . . . . . . . . 16 (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
465464, 142sselid 3992 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (LIndS‘𝐵))
466 eqid 2734 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
467233, 466, 319, 244, 204, 320islinds5 33374 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
468467biimpa 476 . . . . . . . . . . . . . . 15 (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
469208, 365, 465, 468syl21anc 838 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
470 fvexd 6921 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
471 elmapg 8877 . . . . . . . . . . . . . . . 16 (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
472471biimpar 477 . . . . . . . . . . . . . . 15 ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
473470, 142, 251, 472syl21anc 838 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
474463, 469, 473rspcdva 3622 . . . . . . . . . . . . 13 (𝜑 → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
475336, 451, 474mp2and 699 . . . . . . . . . . . 12 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))
476 fconstmpt 5750 . . . . . . . . . . . 12 (𝑌 × {(0g‘(Scalar‘𝐵))}) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵)))
477475, 476eqtrdi 2790 . . . . . . . . . . 11 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))))
478 ovex 7463 . . . . . . . . . . . . 13 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
479478rgenw 3062 . . . . . . . . . . . 12 𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
480 mpteqb 7034 . . . . . . . . . . . 12 (∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵))))
481479, 480ax-mp 5 . . . . . . . . . . 11 ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
482477, 481sylib 218 . . . . . . . . . 10 (𝜑 → ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
483482r19.21bi 3248 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
484312, 445, 3133eqtr3rd 2783 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐴))
485484adantr 480 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g‘(Scalar‘𝐵)) = (0g𝐴))
486202, 483, 4853eqtrd 2778 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))
487183, 486jca 511 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
488186fmpttd 7134 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
489 fvexd 6921 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
490489, 144elmapd 8878 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
491488, 490mpbird 257 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋))
492 simpr 484 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
493492breq1d 5157 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴))))
494 nfv 1911 . . . . . . . . . . . . . 14 𝑖(𝜑𝑗𝑌)
495 nfmpt1 5255 . . . . . . . . . . . . . . 15 𝑖(𝑖𝑋 ↦ (𝑗𝑊𝑖))
496495nfeq2 2920 . . . . . . . . . . . . . 14 𝑖 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
497494, 496nfan 1896 . . . . . . . . . . . . 13 𝑖((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
498 simplr 769 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
499498fveq1d 6908 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → (𝑤𝑖) = ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
500499oveq1d 7445 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → ((𝑤𝑖)( ·𝑠𝐴)𝑖) = (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))
501497, 500mpteq2da 5245 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)))
502501oveq2d 7446 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))))
503502eqeq1d 2736 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴) ↔ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
504493, 503anbi12d 632 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) ↔ ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))))
505492eqeq1d 2736 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))})))
506504, 505imbi12d 344 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) ↔ (((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
507491, 506rspcdv 3613 . . . . . . 7 ((𝜑𝑗𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
508139, 487, 507mp2d 49 . . . . . 6 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
509508, 254eqtrdi 2790 . . . . 5 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
510509, 308sylib 218 . . . 4 ((𝜑𝑗𝑌) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
511510ralrimiva 3143 . . 3 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
512 eqidd 2735 . . . 4 ((𝑗 = 𝑘𝑖 = 𝑙) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴)))
513 fvexd 6921 . . . 4 ((𝜑𝑗𝑌𝑖𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
514 fvexd 6921 . . . 4 ((𝜑𝑘𝑌𝑙𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
515157, 512, 513, 514fnmpoovd 8110 . . 3 (𝜑 → (𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
516511, 515mpbird 257 . 2 (𝜑𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))))
517 fconstmpo 7549 . 2 ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}) = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴)))
518516, 517eqtr4di 2792 1 (𝜑𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  wss 3962  {csn 4630  cop 4636   class class class wbr 5147  cmpt 5230   × cxp 5686  dom cdm 5688  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  cmpo 7432  f cof 7694   supp csupp 8183  m cmap 8864  Fincfn 8983   finSupp cfsupp 9398  Basecbs 17244  s cress 17273  +gcplusg 17297  .rcmulr 17298  Scalarcsca 17300   ·𝑠 cvsca 17301  0gc0g 17485   Σg cgsu 17486  Mndcmnd 18759  Grpcgrp 18963  SubGrpcsubg 19150  CMndccmn 19812  Abelcabl 19813  Ringcrg 20250  SubRingcsubrg 20585  DivRingcdr 20745  LModclmod 20874  LSubSpclss 20946  LBasisclbs 21090  LVecclvec 21118  subringAlg csra 21187   freeLMod cfrlm 21783  LIndSclinds 21842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-fz 13544  df-fzo 13691  df-seq 14039  df-hash 14366  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-hom 17321  df-cco 17322  df-0g 17487  df-gsum 17488  df-prds 17493  df-pws 17495  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-mulg 19098  df-subg 19153  df-ghm 19243  df-cntz 19347  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-nzr 20529  df-subrng 20562  df-subrg 20586  df-drng 20747  df-lmod 20876  df-lss 20947  df-lsp 20987  df-lmhm 21038  df-lbs 21091  df-lvec 21119  df-sra 21189  df-rgmod 21190  df-dsmm 21769  df-frlm 21784  df-uvc 21820  df-lindf 21843  df-linds 21844
This theorem is referenced by:  fedgmul  33658
  Copyright terms: Public domain W3C validator