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

Theorem fedgmullem2 31094
 Description: Lemma for fedgmul 31095. (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 19563 . . . . . . . . . . . . . 14 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
76biimpa 480 . . . . . . . . . . . . 13 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
83, 4, 7syl2anc 587 . . . . . . . . . . . 12 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
98simpld 498 . . . . . . . . . . 11 (𝜑𝑉 ∈ (SubRing‘𝐸))
10 fedgmul.a . . . . . . . . . . . 12 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11 fedgmul.k . . . . . . . . . . . 12 𝐾 = (𝐸s 𝑉)
1210, 11sralvec 31058 . . . . . . . . . . 11 ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
131, 2, 9, 12syl3anc 1368 . . . . . . . . . 10 (𝜑𝐴 ∈ LVec)
14 lveclmod 19880 . . . . . . . . . 10 (𝐴 ∈ LVec → 𝐴 ∈ LMod)
1513, 14syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ LMod)
16 fedgmullem.x . . . . . . . . . . 11 (𝜑𝑋 ∈ (LBasis‘𝐶))
17 eqid 2824 . . . . . . . . . . . 12 (Base‘𝐶) = (Base‘𝐶)
18 eqid 2824 . . . . . . . . . . . 12 (LBasis‘𝐶) = (LBasis‘𝐶)
1917, 18lbsss 19851 . . . . . . . . . . 11 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
2016, 19syl 17 . . . . . . . . . 10 (𝜑𝑋 ⊆ (Base‘𝐶))
21 eqid 2824 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2221subrgss 19538 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
233, 22syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
245, 21ressbas2 16557 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘𝐹))
26 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
2726a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28 eqid 2824 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
2928subrgss 19538 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
304, 29syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3127, 30srabase 19952 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
3225, 31eqtrd 2859 . . . . . . . . . . . 12 (𝜑𝑈 = (Base‘𝐶))
3332, 23eqsstrrd 3992 . . . . . . . . . . 11 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
3410a1i 11 . . . . . . . . . . . 12 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
3521subrgss 19538 . . . . . . . . . . . . 13 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
369, 35syl 17 . . . . . . . . . . . 12 (𝜑𝑉 ⊆ (Base‘𝐸))
3734, 36srabase 19952 . . . . . . . . . . 11 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
3833, 37sseqtrd 3993 . . . . . . . . . 10 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
3920, 38sstrd 3963 . . . . . . . . 9 (𝜑𝑋 ⊆ (Base‘𝐴))
4034, 3, 36srasubrg 31057 . . . . . . . . . . . 12 (𝜑𝑈 ∈ (SubRing‘𝐴))
41 subrgsubg 19543 . . . . . . . . . . . 12 (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
4240, 41syl 17 . . . . . . . . . . 11 (𝜑𝑈 ∈ (SubGrp‘𝐴))
4310, 1, 9drgextvsca 31061 . . . . . . . . . . . . . 14 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
4443oveqdr 7179 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) = (𝑥( ·𝑠𝐴)𝑦))
453adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
468simprd 499 . . . . . . . . . . . . . . . 16 (𝜑𝑉𝑈)
4746adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉𝑈)
48 simprl 770 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49 ressabs 16565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
503, 46, 49syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
515oveq1i 7161 . . . . . . . . . . . . . . . . . . . . 21 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
5250, 51, 113eqtr4g 2884 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = 𝐾)
5327, 30srasca 19955 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
5452, 53eqtr3d 2861 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 = (Scalar‘𝐶))
5554fveq2d 6667 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
5611, 21ressbas2 16557 . . . . . . . . . . . . . . . . . . 19 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
5736, 56syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑉 = (Base‘𝐾))
5834, 36srasca 19955 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
5911, 58syl5eq 2871 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 = (Scalar‘𝐴))
6052, 53, 593eqtr3rd 2868 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
6160fveq2d 6667 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
6255, 57, 613eqtr4d 2869 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 = (Base‘(Scalar‘𝐴)))
6362adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
6448, 63eleqtrrd 2919 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑉)
6547, 64sseldd 3954 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑥𝑈)
66 simprr 772 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → 𝑦𝑈)
67 eqid 2824 . . . . . . . . . . . . . . 15 (.r𝐸) = (.r𝐸)
6867subrgmcl 19549 . . . . . . . . . . . . . 14 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥𝑈𝑦𝑈) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
6945, 65, 66, 68syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥(.r𝐸)𝑦) ∈ 𝑈)
7044, 69eqeltrrd 2917 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦𝑈)) → (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
7170ralrimivva 3186 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)
72 eqid 2824 . . . . . . . . . . . . 13 (Scalar‘𝐴) = (Scalar‘𝐴)
73 eqid 2824 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74 eqid 2824 . . . . . . . . . . . . 13 (Base‘𝐴) = (Base‘𝐴)
75 eqid 2824 . . . . . . . . . . . . 13 ( ·𝑠𝐴) = ( ·𝑠𝐴)
76 eqid 2824 . . . . . . . . . . . . 13 (LSubSp‘𝐴) = (LSubSp‘𝐴)
7772, 73, 74, 75, 76islss4 19736 . . . . . . . . . . . 12 (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)))
7877biimpar 481 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦𝑈 (𝑥( ·𝑠𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
7915, 42, 71, 78syl12anc 835 . . . . . . . . . 10 (𝜑𝑈 ∈ (LSubSp‘𝐴))
8020, 32sseqtrrd 3994 . . . . . . . . . 10 (𝜑𝑋𝑈)
8118lbslinds 20531 . . . . . . . . . . . 12 (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
8281, 16sseldi 3951 . . . . . . . . . . 11 (𝜑𝑋 ∈ (LIndS‘𝐶))
8323, 37sseqtrd 3993 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐴))
84 eqid 2824 . . . . . . . . . . . . . . 15 (𝐴s 𝑈) = (𝐴s 𝑈)
8584, 74ressbas2 16557 . . . . . . . . . . . . . 14 (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴s 𝑈)))
8683, 85syl 17 . . . . . . . . . . . . 13 (𝜑𝑈 = (Base‘(𝐴s 𝑈)))
8725, 86, 313eqtr3rd 2868 . . . . . . . . . . . 12 (𝜑 → (Base‘𝐶) = (Base‘(𝐴s 𝑈)))
8884, 72resssca 16652 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
893, 88syl 17 . . . . . . . . . . . . . 14 (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴s 𝑈)))
9060, 89eqtr3d 2861 . . . . . . . . . . . . 13 (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴s 𝑈)))
9190fveq2d 6667 . . . . . . . . . . . 12 (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴s 𝑈))))
9290fveq2d 6667 . . . . . . . . . . . 12 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘(𝐴s 𝑈))))
93 eqid 2824 . . . . . . . . . . . . . . . . 17 (+g𝐸) = (+g𝐸)
945, 93ressplusg 16614 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐸) = (+g𝐹))
953, 94syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐹))
9634, 36sraaddg 19953 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐸) = (+g𝐴))
9727, 30sraaddg 19953 . . . . . . . . . . . . . . 15 (𝜑 → (+g𝐹) = (+g𝐶))
9895, 96, 973eqtr3rd 2868 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐶) = (+g𝐴))
99 eqid 2824 . . . . . . . . . . . . . . . 16 (+g𝐴) = (+g𝐴)
10084, 99ressplusg 16614 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → (+g𝐴) = (+g‘(𝐴s 𝑈)))
1013, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (+g𝐴) = (+g‘(𝐴s 𝑈)))
10298, 101eqtrd 2859 . . . . . . . . . . . . 13 (𝜑 → (+g𝐶) = (+g‘(𝐴s 𝑈)))
103102oveqdr 7179 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g𝐶)𝑦) = (𝑥(+g‘(𝐴s 𝑈))𝑦))
104 fedgmul.2 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ DivRing)
10552, 2eqeltrd 2916 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
106 eqid 2824 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
10726, 106sralvec 31058 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108104, 105, 4, 107syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
109 lveclmod 19880 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110108, 109syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
111 eqid 2824 . . . . . . . . . . . . . . 15 (Scalar‘𝐶) = (Scalar‘𝐶)
112 eqid 2824 . . . . . . . . . . . . . . 15 ( ·𝑠𝐶) = ( ·𝑠𝐶)
113 eqid 2824 . . . . . . . . . . . . . . 15 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
11417, 111, 112, 113lmodvscl 19653 . . . . . . . . . . . . . 14 ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
1151143expb 1117 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
116110, 115sylan 583 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) ∈ (Base‘𝐶))
117 fedgmul.b . . . . . . . . . . . . . . . 16 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118117, 1, 3drgextvsca 31061 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
11943, 118eqtr3d 2861 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠𝐵))
12084, 75ressvsca 16653 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1213, 120syl 17 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐴) = ( ·𝑠 ‘(𝐴s 𝑈)))
1225, 67ressmulr 16627 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
1233, 122syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐸) = (.r𝐹))
12426, 104, 4drgextvsca 31061 . . . . . . . . . . . . . . 15 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
125123, 118, 1243eqtr3d 2867 . . . . . . . . . . . . . 14 (𝜑 → ( ·𝑠𝐵) = ( ·𝑠𝐶))
126119, 121, 1253eqtr3rd 2868 . . . . . . . . . . . . 13 (𝜑 → ( ·𝑠𝐶) = ( ·𝑠 ‘(𝐴s 𝑈)))
127126oveqdr 7179 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠𝐶)𝑦) = (𝑥( ·𝑠 ‘(𝐴s 𝑈))𝑦))
128 ovexd 7186 . . . . . . . . . . . 12 (𝜑 → (𝐴s 𝑈) ∈ V)
12987, 91, 92, 103, 116, 127, 108, 128lindspropd 30989 . . . . . . . . . . 11 (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴s 𝑈)))
13082, 129eleqtrd 2918 . . . . . . . . . 10 (𝜑𝑋 ∈ (LIndS‘(𝐴s 𝑈)))
13176, 84lsslinds 20529 . . . . . . . . . . 11 ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) → (𝑋 ∈ (LIndS‘(𝐴s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132131biimpa 480 . . . . . . . . . 10 (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
13315, 79, 80, 130, 132syl31anc 1370 . . . . . . . . 9 (𝜑𝑋 ∈ (LIndS‘𝐴))
134 eqid 2824 . . . . . . . . . . 11 (0g𝐴) = (0g𝐴)
135 eqid 2824 . . . . . . . . . . 11 (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
13674, 73, 72, 75, 134, 135islinds5 30975 . . . . . . . . . 10 ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
137136biimpa 480 . . . . . . . . 9 (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
13815, 39, 133, 137syl21anc 836 . . . . . . . 8 (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
139138adantr 484 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
140 eqid 2824 . . . . . . . . . 10 (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
141 fvexd 6678 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (0g𝐹) ∈ V)
142 fedgmullem.y . . . . . . . . . . 11 (𝜑𝑌 ∈ (LBasis‘𝐵))
143142adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑌 ∈ (LBasis‘𝐵))
14416adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145 fedgmullem2.1 . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146 fvexd 6678 . . . . . . . . . . . . . . . 16 (𝜑 → (Scalar‘𝐴) ∈ V)
147142, 16xpexd 7470 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 × 𝑋) ∈ V)
148 eqid 2824 . . . . . . . . . . . . . . . . 17 ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149 eqid 2824 . . . . . . . . . . . . . . . . 17 (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150148, 73, 135, 149frlmelbas 20454 . . . . . . . . . . . . . . . 16 (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
151146, 147, 150syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
152145, 151mpbid 235 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴))))
153152simpld 498 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
154 fvexd 6678 . . . . . . . . . . . . . 14 (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155154, 147elmapd 8418 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156153, 155mpbid 235 . . . . . . . . . . . 12 (𝜑𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157156ffnd 6506 . . . . . . . . . . 11 (𝜑𝑊 Fn (𝑌 × 𝑋))
158157adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159 simpr 488 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑗𝑌)
160152simprd 499 . . . . . . . . . . . 12 (𝜑𝑊 finSupp (0g‘(Scalar‘𝐴)))
161 drngring 19511 . . . . . . . . . . . . . . . 16 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
1621, 161syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ Ring)
163 ringmnd 19309 . . . . . . . . . . . . . . 15 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164162, 163syl 17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ Mnd)
165 subrgsubg 19543 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
1669, 165syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑉 ∈ (SubGrp‘𝐸))
167 eqid 2824 . . . . . . . . . . . . . . . . 17 (0g𝐸) = (0g𝐸)
168167subg0cl 18289 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (SubGrp‘𝐸) → (0g𝐸) ∈ 𝑉)
169166, 168syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0g𝐸) ∈ 𝑉)
17046, 169sseldd 3954 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) ∈ 𝑈)
1715, 21, 167ress0g 17941 . . . . . . . . . . . . . 14 ((𝐸 ∈ Mnd ∧ (0g𝐸) ∈ 𝑈𝑈 ⊆ (Base‘𝐸)) → (0g𝐸) = (0g𝐹))
172164, 170, 23, 171syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g𝐹))
17354fveq2d 6667 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
17411, 167subrg0 19544 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
1759, 174syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0g𝐸) = (0g𝐾))
17660fveq2d 6667 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
177173, 175, 1763eqtr4d 2869 . . . . . . . . . . . . 13 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
178172, 177eqtr3d 2861 . . . . . . . . . . . 12 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐴)))
179160, 178breqtrrd 5081 . . . . . . . . . . 11 (𝜑𝑊 finSupp (0g𝐹))
180179adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑌) → 𝑊 finSupp (0g𝐹))
181140, 141, 143, 144, 158, 159, 180fsuppcurry1 30482 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g𝐹))
182178adantr 484 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g𝐹) = (0g‘(Scalar‘𝐴)))
183181, 182breqtrd 5079 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)))
184 eqidd 2825 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
185156fovrnda 7315 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186185anassrs 471 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187184, 186fvmpt2d 6774 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188187oveq1d 7166 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
189119ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
190189oveqd 7168 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
191188, 190eqtrd 2859 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
192191mpteq2dva 5148 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
193192oveq2d 7167 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1941adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐸 ∈ DivRing)
1959adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑉 ∈ (SubRing‘𝐸))
1962adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐾 ∈ DivRing)
19710, 194, 195, 11, 196, 144drgextgsum 31065 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
1983adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199104adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐹 ∈ DivRing)
200117, 194, 198, 5, 199, 144drgextgsum 31065 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
201197, 200eqtr3d 2861 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
202193, 201eqtrd 2859 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
203142mptexd 6980 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ V)
204 eqid 2824 . . . . . . . . . . . . . . . . . 18 (0g𝐵) = (0g𝐵)
205117, 5sralvec 31058 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
2061, 104, 3, 205syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ LVec)
207 lveclmod 19880 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ LMod)
209208adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐵 ∈ LMod)
210 lmodabl 19683 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝐵 ∈ Abel)
212117a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213212, 3, 23srasubrg 31057 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ (SubRing‘𝐵))
214 subrgsubg 19543 . . . . . . . . . . . . . . . . . . . 20 (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215213, 214syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 ∈ (SubGrp‘𝐵))
216215adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217110ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
21861ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219186, 218eleqtrd 2918 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
22020ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
221 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
222220, 221sseldd 3954 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
22317, 111, 112, 113lmodvscl 19653 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
224217, 219, 222, 223syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
225125oveqd 7168 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
226225ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐶)𝑖))
22732ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
228224, 226, 2273eltr4d 2931 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) ∈ 𝑈)
229228fmpttd 6872 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)):𝑋𝑈)
230212, 23srasca 19955 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
2315, 230syl5eq 2871 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹 = (Scalar‘𝐵))
232231adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝐹 = (Scalar‘𝐵))
233 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (Base‘𝐵) = (Base‘𝐵)
234 ovexd 7186 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
23520, 33sstrd 3963 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ⊆ (Base‘𝐸))
236235adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237 simprr 772 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
238236, 237sseldd 3954 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑖 ∈ (Base‘𝐸))
239238anassrs 471 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
240212, 23srabase 19952 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241240ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐵))
242239, 241eleqtrd 2918 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
243 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (0g𝐹) = (0g𝐹)
244 eqid 2824 . . . . . . . . . . . . . . . . . . 19 ( ·𝑠𝐵) = ( ·𝑠𝐵)
245144, 209, 232, 233, 234, 242, 204, 243, 244, 181mptscmfsupp0 19701 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) finSupp (0g𝐵))
246204, 211, 144, 216, 229, 245gsumsubgcl 19042 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ 𝑈)
247231fveq2d 6667 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
24825, 247eqtrd 2859 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘(Scalar‘𝐵)))
249248adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250246, 249eleqtrd 2918 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251250fmpttd 6872 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252251ffund 6509 . . . . . . . . . . . . . 14 (𝜑 → Fun (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
253 fvexd 6678 . . . . . . . . . . . . . 14 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
254 fconstmpt 5602 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × {(0g‘(Scalar‘𝐴))}) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴)))
255254eqeq2i 2837 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
256 ovex 7184 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑊𝑖) ∈ V
257256rgenw 3145 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑋 (𝑘𝑊𝑖) ∈ V
258 mpteqb 6780 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑖𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
259257, 258ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
260255, 259bitri 278 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
261260necon3abii 3060 . . . . . . . . . . . . . . . . . 18 ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
262 df-ov 7154 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263262eqcomi 2833 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264263a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265264eqeq1d 2826 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
266265necon3abid 3050 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝑌) ∧ 𝑖𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
267266rexbidva 3288 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
268 rexnal 3232 . . . . . . . . . . . . . . . . . . 19 (∃𝑖𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
269267, 268syl6rbb 291 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (¬ ∀𝑖𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
270261, 269syl5bb 286 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑌) → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
271270rabbidva 3463 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))})
272 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273272neeq1d 3073 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊𝑧) ≠ (0g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
274273dmrab 30276 . . . . . . . . . . . . . . . 16 dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} = {𝑘𝑌 ∣ ∃𝑖𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))}
275271, 274eqtr4di 2877 . . . . . . . . . . . . . . 15 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
276 fvexd 6678 . . . . . . . . . . . . . . . . . 18 (𝜑 → (0g‘(Scalar‘𝐴)) ∈ V)
277 suppvalfn 7835 . . . . . . . . . . . . . . . . . 18 ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
278157, 147, 276, 277syl3anc 1368 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))})
279160fsuppimpd 8839 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) ∈ Fin)
280278, 279eqeltrrd 2917 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
281 dmfi 8801 . . . . . . . . . . . . . . . 16 ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
282280, 281syl 17 . . . . . . . . . . . . . . 15 (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
283275, 282eqeltrd 2916 . . . . . . . . . . . . . 14 (𝜑 → {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin)
284 nfv 1916 . . . . . . . . . . . . . . . . . . 19 𝑖𝜑
285 nfcv 2982 . . . . . . . . . . . . . . . . . . . . 21 𝑖𝑌
286 nfmpt1 5151 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖))
287 nfcv 2982 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖(𝑋 × {(0g‘(Scalar‘𝐴))})
288286, 287nfne 3114 . . . . . . . . . . . . . . . . . . . . . 22 𝑖(𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})
289288, 285nfrabw 3376 . . . . . . . . . . . . . . . . . . . . 21 𝑖{𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}
290285, 289nfdif 4088 . . . . . . . . . . . . . . . . . . . 20 𝑖(𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
291290nfcri 2969 . . . . . . . . . . . . . . . . . . 19 𝑖 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
292284, 291nfan 1901 . . . . . . . . . . . . . . . . . 18 𝑖(𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
293 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
294293eldifad 3931 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗𝑌)
295293eldifbd 3932 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
296 oveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297296mpteq2dv 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑗 → (𝑖𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
298297neeq1d 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑗 → ((𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
299298elrab 3666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ↔ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
300295, 299sylnib 331 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗𝑌 ∧ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
301294, 300mpnanrd 413 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}))
302 nne 3018 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
303301, 302sylib 221 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
304303, 254syl6eq 2875 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
305 ovex 7184 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑊𝑖) ∈ V
306305rgenw 3145 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖𝑋 (𝑗𝑊𝑖) ∈ V
307 mpteqb 6780 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
308306, 307ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
309304, 308sylib 221 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
310309r19.21bi 3203 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
311310oveq1d 7166 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖))
312117, 1, 3drgext0g 31060 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐸) = (0g𝐵))
313117, 1, 3drgext0gsca 31062 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0g𝐵) = (0g‘(Scalar‘𝐵)))
314312, 177, 3133eqtr3d 2867 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
315314ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
316315oveq1d 7166 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐴))( ·𝑠𝐵)𝑖) = ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖))
317208ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝐵 ∈ LMod)
318294, 242syldanl 604 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐵))
319 eqid 2824 . . . . . . . . . . . . . . . . . . . . 21 (Scalar‘𝐵) = (Scalar‘𝐵)
320 eqid 2824 . . . . . . . . . . . . . . . . . . . . 21 (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
321233, 319, 244, 320, 204lmod0vs 19669 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
322317, 318, 321syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((0g‘(Scalar‘𝐵))( ·𝑠𝐵)𝑖) = (0g𝐵))
323311, 316, 3223eqtrd 2863 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖) = (0g𝐵))
324292, 323mpteq2da 5147 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)) = (𝑖𝑋 ↦ (0g𝐵)))
325324oveq2d 7167 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))))
326208, 210syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ Abel)
327 ablgrp 18913 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Abel → 𝐵 ∈ Grp)
328 grpmnd 18112 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
329326, 327, 3283syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ Mnd)
330204gsumz 18002 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
331329, 16, 330syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
332331adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ (0g𝐵))) = (0g𝐵))
333313adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (0g𝐵) = (0g‘(Scalar‘𝐵)))
334325, 332, 3333eqtrd 2863 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑌 ∖ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
335334, 142suppss2 7862 . . . . . . . . . . . . . 14 (𝜑 → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘𝑌 ∣ (𝑖𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
336 suppssfifsupp 8847 . . . . . . . . . . . . . 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 1375 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
338 eqidd 2825 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))))
339 ovexd 7186 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V)
340338, 339fvmpt2d 6774 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
341340oveq1d 7166 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑌) → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
342341mpteq2dva 5148 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
343342oveq2d 7167 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
344119adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → ( ·𝑠𝐴) = ( ·𝑠𝐵))
34543ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (.r𝐸) = ( ·𝑠𝐴))
346345oveqd 7168 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))
347346mpteq2dva 5148 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))
348118adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
349348oveqd 7168 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))
350349mpteq2dv 5149 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
351347, 350eqtr3d 2861 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))
352351oveq2d 7167 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
353 eqidd 2825 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → 𝑗 = 𝑗)
354344, 352, 353oveq123d 7172 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
355201oveq1d 7166 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
356354, 355eqtrd 2859 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗) = ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))
357356mpteq2dva 5148 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)) = (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗)))
358357oveq2d 7167 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
35910, 21sraring 31055 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
360162, 36, 359syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ Ring)
361 ringcmn 19336 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
362360, 361syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ CMnd)
363162adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝐸 ∈ Ring)
364 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (LBasis‘𝐵) = (LBasis‘𝐵)
365233, 364lbsss 19851 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
366142, 365syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑌 ⊆ (Base‘𝐵))
367366, 240sseqtrrd 3994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑌 ⊆ (Base‘𝐸))
368367adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑌 ⊆ (Base‘𝐸))
369 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗𝑌)
370368, 369sseldd 3954 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → 𝑗 ∈ (Base‘𝐸))
37121, 67ringcl 19316 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
372363, 238, 370, 371syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
37337adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (Base‘𝐸) = (Base‘𝐴))
374372, 373eleqtrd 2918 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
375374ralrimivva 3186 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
376 fedgmullem.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
377376fmpo 7763 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378375, 377sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
37972, 73, 75, 74, 15, 156, 378, 147lcomf 19675 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
38072, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160lcomfsupp 19676 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) finSupp (0g𝐴))
38174, 134, 362, 142, 16, 379, 380gsumxp 19098 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))))
382 fedgmullem2.2 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑊f ( ·𝑠𝐴)𝐷)) = (0g𝐴))
3831623ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝐸 ∈ Ring)
3841563ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
38557, 55eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
386385, 36eqsstrrd 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
38761, 386eqsstrd 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
388387, 37sseqtrd 3993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
3893883ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390384, 389fssd 6520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
391 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗𝑌)
392 simp3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖𝑋)
393390, 391, 392fovrnd 7316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
394373ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗𝑌𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
395393, 394eleqtrrd 2919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
3962383impb 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
3973703impb 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗𝑌𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
39821, 67ringass 19319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
399383, 395, 396, 397, 398syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
400399mpoeq3dva 7226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
401 ovexd 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑗𝑊𝑖) ∈ V)
402 ovexd 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
403 fnov 7277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
404157, 403sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑊 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑗𝑊𝑖)))
405376a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
406142, 16, 401, 402, 404, 405offval22 7781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
407 ofeq 7407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((.r𝐸) = ( ·𝑠𝐴) → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
40843, 407syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
409408oveqd 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑊f (.r𝐸)𝐷) = (𝑊f ( ·𝑠𝐴)𝐷))
410400, 406, 4093eqtr2rd 2866 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
411410ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑊f ( ·𝑠𝐴)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
412411oveqd 7168 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖))
413 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
414 ovexd 7186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V)
415 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
416415ovmpt4g 7292 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑌𝑖𝑋 ∧ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
417413, 221, 414, 416syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
418412, 417eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))
419418mpteq2dva 5148 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) = (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)))
420419oveq2d 7167 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))))
421162adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
422367sselda 3953 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
423162ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
424386ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
425424, 219sseldd 3954 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
42621, 67ringcl 19316 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
427423, 425, 239, 426syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝑗𝑊𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
428312adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (0g𝐸) = (0g𝐵))
429245, 350, 4283brtr4d 5085 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
43021, 167, 93, 67, 421, 144, 422, 427, 429gsummulc1 19361 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝑗𝑊𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
431420, 430eqtrd 2859 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
432144mptexd 6980 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)) ∈ V)
43315adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝐴 ∈ LMod)
43436adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → 𝑉 ⊆ (Base‘𝐸))
43510, 432, 194, 433, 434gsumsra 30727 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))
436144mptexd 6980 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)) ∈ V)
43710, 436, 194, 433, 434gsumsra 30727 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))))
438437oveq1d 7166 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
43943adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐴))
440347oveq2d 7167 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖))))
441439, 440, 353oveq123d 7172 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗𝑌) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
442438, 441eqtrd 2859 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
443431, 435, 4423eqtr3d 2867 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))
444443mpteq2dva 5148 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖)))) = (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗)))
445444oveq2d 7167 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ (𝐴 Σg (𝑖𝑋 ↦ (𝑗(𝑊f ( ·𝑠𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))))
446381, 382, 4453eqtr3rd 2868 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐴))
44710, 1, 9drgext0g 31060 . . . . . . . . . . . . . . . 16 (𝜑 → (0g𝐸) = (0g𝐴))
448446, 447, 3123eqtr2d 2865 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐴 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐴)𝑖)))( ·𝑠𝐴)𝑗))) = (0g𝐵))
44910, 1, 9, 11, 2, 142drgextgsum 31065 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
450117, 1, 3, 5, 104, 142drgextgsum 31065 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
451449, 450eqtr3d 2861 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))))
452358, 448, 4513eqtr3rd 2868 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ ((𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))( ·𝑠𝐵)𝑗))) = (0g𝐵))
453343, 452eqtrd 2859 . . . . . . . . . . . . 13 (𝜑 → (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))
454 breq1 5056 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 finSupp (0g‘(Scalar‘𝐵)) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵))))
455 nfmpt1 5151 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
456455nfeq2 2999 . . . . . . . . . . . . . . . . . . 19 𝑗 𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))
457 fveq1 6662 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏𝑗) = ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗))
458457oveq1d 7166 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
459458adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∧ 𝑗𝑌) → ((𝑏𝑗)( ·𝑠𝐵)𝑗) = (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))
460456, 459mpteq2da 5147 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗)))
461460oveq2d 7167 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))))
462461eqeq1d 2826 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵) ↔ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)))
463454, 462anbi12d 633 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → ((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) ↔ ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵))))
464 eqeq1 2828 . . . . . . . . . . . . . . 15 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
465463, 464imbi12d 348 . . . . . . . . . . . . . 14 (𝑏 = (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) → (((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})) ↔ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
466364lbslinds 20531 . . . . . . . . . . . . . . . 16 (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
467466, 142sseldi 3951 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (LIndS‘𝐵))
468 eqid 2824 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
469233, 468, 319, 244, 204, 320islinds5 30975 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
470469biimpa 480 . . . . . . . . . . . . . . 15 (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
471208, 366, 467, 470syl21anc 836 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ ((𝑏𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
472 fvexd 6678 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
473 elmapg 8417 . . . . . . . . . . . . . . . 16 (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌) ↔ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
474473biimpar 481 . . . . . . . . . . . . . . 15 ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
475472, 142, 251, 474syl21anc 836 . . . . . . . . . . . . . 14 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
476465, 471, 475rspcdva 3611 . . . . . . . . . . . . 13 (𝜑 → (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗𝑌 ↦ (((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))))‘𝑗)( ·𝑠𝐵)𝑗))) = (0g𝐵)) → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
477337, 453, 476mp2and 698 . . . . . . . . . . . 12 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))
478 fconstmpt 5602 . . . . . . . . . . . 12 (𝑌 × {(0g‘(Scalar‘𝐵))}) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵)))
479477, 478syl6eq 2875 . . . . . . . . . . 11 (𝜑 → (𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))))
480 ovex 7184 . . . . . . . . . . . . 13 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
481480rgenw 3145 . . . . . . . . . . . 12 𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V
482 mpteqb 6780 . . . . . . . . . . . 12 (∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) ∈ V → ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵))))
483481, 482ax-mp 5 . . . . . . . . . . 11 ((𝑗𝑌 ↦ (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖)))) = (𝑗𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
484479, 483sylib 221 . . . . . . . . . 10 (𝜑 → ∀𝑗𝑌 (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
485484r19.21bi 3203 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐵 Σg (𝑖𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
486312, 447, 3133eqtr3rd 2868 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐴))
487486adantr 484 . . . . . . . . 9 ((𝜑𝑗𝑌) → (0g‘(Scalar‘𝐵)) = (0g𝐴))
488202, 485, 4873eqtrd 2863 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))
489183, 488jca 515 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
490186fmpttd 6872 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
491 fvexd 6678 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
492491, 144elmapd 8418 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
493490, 492mpbird 260 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋))
494 simpr 488 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
495494breq1d 5063 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴))))
496 nfv 1916 . . . . . . . . . . . . . 14 𝑖(𝜑𝑗𝑌)
497 nfmpt1 5151 . . . . . . . . . . . . . . 15 𝑖(𝑖𝑋 ↦ (𝑗𝑊𝑖))
498497nfeq2 2999 . . . . . . . . . . . . . 14 𝑖 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))
499496, 498nfan 1901 . . . . . . . . . . . . 13 𝑖((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
500 simplr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖)))
501500fveq1d 6665 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → (𝑤𝑖) = ((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
502501oveq1d 7166 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖𝑋) → ((𝑤𝑖)( ·𝑠𝐴)𝑖) = (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))
503499, 502mpteq2da 5147 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖)) = (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖)))
504503oveq2d 7167 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))))
505504eqeq1d 2826 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴) ↔ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)))
506495, 505anbi12d 633 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) ↔ ((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴))))
507494eqeq1d 2826 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))})))
508506, 507imbi12d 348 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑤 = (𝑖𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) ↔ (((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
509493, 508rspcdv 3601 . . . . . . 7 ((𝜑𝑗𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ ((𝑤𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) → (((𝑖𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖𝑋 ↦ (((𝑖𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠𝐴)𝑖))) = (0g𝐴)) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
510139, 489, 509mp2d 49 . . . . . 6 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
511510, 254syl6eq 2875 . . . . 5 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖𝑋 ↦ (0g‘(Scalar‘𝐴))))
512511, 308sylib 221 . . . 4 ((𝜑𝑗𝑌) → ∀𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
513512ralrimiva 3177 . . 3 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
514 eqidd 2825 . . . 4 ((𝑗 = 𝑘𝑖 = 𝑙) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴)))
515 fvexd 6678 . . . 4 ((𝜑𝑗𝑌𝑖𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
516 fvexd 6678 . . . 4 ((𝜑𝑘𝑌𝑙𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
517157, 514, 515, 516fnmpoovd 7780 . . 3 (𝜑 → (𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑗𝑌𝑖𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
518513, 517mpbird 260 . 2 (𝜑𝑊 = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴))))
519 fconstmpo 7264 . 2 ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}) = (𝑘𝑌, 𝑙𝑋 ↦ (0g‘(Scalar‘𝐴)))
520518, 519eqtr4di 2877 1 (𝜑𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  {crab 3137  Vcvv 3480   ∖ cdif 3916   ⊆ wss 3919  {csn 4550  ⟨cop 4556   class class class wbr 5053   ↦ cmpt 5133   × cxp 5541  dom cdm 5543  Fun wfun 6339   Fn wfn 6340  ⟶wf 6341  ‘cfv 6345  (class class class)co 7151   ∈ cmpo 7153   ∘f cof 7403   supp csupp 7828   ↑m cmap 8404  Fincfn 8507   finSupp cfsupp 8832  Basecbs 16485   ↾s cress 16486  +gcplusg 16567  .rcmulr 16568  Scalarcsca 16570   ·𝑠 cvsca 16571  0gc0g 16715   Σg cgsu 16716  Mndcmnd 17913  Grpcgrp 18105  SubGrpcsubg 18275  CMndccmn 18908  Abelcabl 18909  Ringcrg 19299  DivRingcdr 19504  SubRingcsubrg 19533  LModclmod 19636  LSubSpclss 19705  LBasisclbs 19848  LVecclvec 19876  subringAlg csra 19942   freeLMod cfrlm 20444  LIndSclinds 20503 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7405  df-om 7577  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-map 8406  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-sup 8905  df-oi 8973  df-card 9367  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11637  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-fz 12897  df-fzo 13040  df-seq 13376  df-hash 13698  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-hom 16591  df-cco 16592  df-0g 16717  df-gsum 16718  df-prds 16723  df-pws 16725  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-mhm 17958  df-submnd 17959  df-grp 18108  df-minusg 18109  df-sbg 18110  df-mulg 18227  df-subg 18278  df-ghm 18358  df-cntz 18449  df-cmn 18910  df-abl 18911  df-mgp 19242  df-ur 19254  df-ring 19301  df-drng 19506  df-subrg 19535  df-lmod 19638  df-lss 19706  df-lsp 19746  df-lmhm 19796  df-lbs 19849  df-lvec 19877  df-sra 19946  df-rgmod 19947  df-nzr 20033  df-dsmm 20430  df-frlm 20445  df-uvc 20481  df-lindf 20504  df-linds 20505 This theorem is referenced by:  fedgmul  31095
 Copyright terms: Public domain W3C validator