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

Theorem fedgmullem1 32714
Description: Lemma for fedgmul 32716. (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‘𝐵))
fedgmullem1.a (𝜑𝑍 ∈ (Base‘𝐴))
fedgmullem1.l (𝜑𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
fedgmullem1.1 (𝜑𝐿 finSupp (0g‘(Scalar‘𝐵)))
fedgmullem1.z (𝜑𝑍 = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
fedgmullem1.g (𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
fedgmullem1.2 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)))
fedgmullem1.3 ((𝜑𝑗𝑌) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
Assertion
Ref Expression
fedgmullem1 (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷))))
Distinct variable groups:   𝐴,𝑖,𝑗   𝐵,𝑗   𝐶,𝑖,𝑗   𝐷,𝑖,𝑗   𝑖,𝐸,𝑗   𝑖,𝐺,𝑗   𝑖,𝐻,𝑗   𝑗,𝐿   𝑈,𝑖   𝑖,𝑋,𝑗   𝑖,𝑌,𝑗   𝜑,𝑖,𝑗
Allowed substitution hints:   𝐵(𝑖)   𝑈(𝑗)   𝐹(𝑖,𝑗)   𝐾(𝑖,𝑗)   𝐿(𝑖)   𝑉(𝑖,𝑗)   𝑍(𝑖,𝑗)

Proof of Theorem fedgmullem1
Dummy variables 𝑢 𝑘 𝑙 𝑔 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fedgmullem1.g . . . . 5 (𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
2 simpllr 775 . . . . . . . . . . . . 13 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
3 simplr 768 . . . . . . . . . . . . 13 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
42, 3ffvelcdmd 7088 . . . . . . . . . . . 12 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5 elmapi 8843 . . . . . . . . . . . 12 ((𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
64, 5syl 17 . . . . . . . . . . 11 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
76anasss 468 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
8 simprr 772 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
97, 8ffvelcdmd 7088 . . . . . . . . 9 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
10 fedgmul.k . . . . . . . . . . . . 13 𝐾 = (𝐸s 𝑉)
11 fedgmul.a . . . . . . . . . . . . . . 15 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 = ((subringAlg ‘𝐸)‘𝑉))
13 fedgmul.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑈 ∈ (SubRing‘𝐸))
14 fedgmul.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 ∈ (SubRing‘𝐹))
15 fedgmul.f . . . . . . . . . . . . . . . . . . 19 𝐹 = (𝐸s 𝑈)
1615subsubrg 20345 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
1716biimpa 478 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1813, 14, 17syl2anc 585 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1918simpld 496 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (SubRing‘𝐸))
20 eqid 2733 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2120subrgss 20320 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
2219, 21syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐸))
2312, 22srasca 20798 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
2410, 23eqtrid 2785 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐴))
2518simprd 497 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑈)
26 ressabs 17194 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2713, 25, 26syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2815oveq1i 7419 . . . . . . . . . . . . . 14 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
2927, 28, 103eqtr4g 2798 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = 𝐾)
30 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
3130a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
32 eqid 2733 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
3332subrgss 20320 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
3414, 33syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3531, 34srasca 20798 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
3629, 35eqtr3d 2775 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐶))
3724, 36eqtr3d 2775 . . . . . . . . . . 11 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
3837fveq2d 6896 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
3938ad2antrr 725 . . . . . . . . 9 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
409, 39eleqtrrd 2837 . . . . . . . 8 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
4140ralrimivva 3201 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
42 fedgmullem.h . . . . . . . 8 𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
4342fmpo 8054 . . . . . . 7 (∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
4441, 43sylib 217 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45 fvexd 6907 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (Base‘(Scalar‘𝐴)) ∈ V)
46 fedgmullem.y . . . . . . . . 9 (𝜑𝑌 ∈ (LBasis‘𝐵))
47 fedgmullem.x . . . . . . . . 9 (𝜑𝑋 ∈ (LBasis‘𝐶))
4846, 47xpexd 7738 . . . . . . . 8 (𝜑 → (𝑌 × 𝑋) ∈ V)
4948adantr 482 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝑌 × 𝑋) ∈ V)
5045, 49elmapd 8834 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
5144, 50mpbird 257 . . . . 5 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
521, 51mpdan 686 . . . 4 (𝜑𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
53 simpl 484 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝜑)
5453adantr 482 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝜑)
551ffvelcdmda 7087 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5655, 5syl 17 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5756adantr 482 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5838feq3d 6705 . . . . . . . . . . 11 (𝜑 → ((𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)) ↔ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))))
5958biimpar 479 . . . . . . . . . 10 ((𝜑 ∧ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
6054, 57, 59syl2anc 585 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
61 simpr 486 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
6260, 61ffvelcdmd 7088 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6362ralrimiva 3147 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6463ralrimiva 3147 . . . . . 6 (𝜑 → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6564, 43sylib 217 . . . . 5 (𝜑𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
6665ffund 6722 . . . 4 (𝜑 → Fun 𝐻)
67 fedgmul.1 . . . . . 6 (𝜑𝐸 ∈ DivRing)
68 drngring 20364 . . . . . 6 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
6967, 68syl 17 . . . . 5 (𝜑𝐸 ∈ Ring)
70 ringgrp 20061 . . . . 5 (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71 eqid 2733 . . . . . 6 (0g𝐸) = (0g𝐸)
7220, 71grpidcl 18850 . . . . 5 (𝐸 ∈ Grp → (0g𝐸) ∈ (Base‘𝐸))
7369, 70, 723syl 18 . . . 4 (𝜑 → (0g𝐸) ∈ (Base‘𝐸))
74 fedgmullem1.1 . . . . . . 7 (𝜑𝐿 finSupp (0g‘(Scalar‘𝐵)))
7574fsuppimpd 9369 . . . . . 6 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ∈ Fin)
76 simpl 484 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝜑)
77 simpr 486 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵)))))
7877eldifad 3961 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗𝑌)
79 fedgmullem1.l . . . . . . . . . 10 (𝜑𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
80 ssidd 4006 . . . . . . . . . 10 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
81 fvexd 6907 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
8279, 80, 46, 81suppssr 8181 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿𝑗) = (0g‘(Scalar‘𝐵)))
83 fedgmullem1.3 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
8478, 83syldan 592 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
85 fedgmul.b . . . . . . . . . . . . . . 15 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
8685a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
8720subrgss 20320 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
8986, 88srasca 20798 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
9015, 89eqtrid 2785 . . . . . . . . . . . 12 (𝜑𝐹 = (Scalar‘𝐵))
9190fveq2d 6896 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐵)))
92 fedgmul.2 . . . . . . . . . . . 12 (𝜑𝐹 ∈ DivRing)
9330, 92, 14drgext0g 32677 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g𝐶))
9491, 93eqtr3d 2775 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9594adantr 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9682, 84, 953eqtr3d 2781 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))
97 fedgmullem1.2 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)))
98 breq1 5152 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → (𝑔 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))))
99 fveq1 6891 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝐺𝑗) → (𝑔𝑖) = ((𝐺𝑗)‘𝑖))
10099oveq1d 7424 . . . . . . . . . . . . . . . 16 (𝑔 = (𝐺𝑗) → ((𝑔𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))
101100mpteq2dv 5251 . . . . . . . . . . . . . . 15 (𝑔 = (𝐺𝑗) → (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
102101oveq2d 7425 . . . . . . . . . . . . . 14 (𝑔 = (𝐺𝑗) → (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
103102eqeq1d 2735 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → ((𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) ↔ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)))
10498, 103anbi12d 632 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → ((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) ↔ ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))))
105 eqeq1 2737 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → (𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}) ↔ (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
106104, 105imbi12d 345 . . . . . . . . . . 11 (𝑔 = (𝐺𝑗) → (((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})) ↔ (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
107 fedgmul.3 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ DivRing)
10829, 107eqeltrd 2834 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
109 eqid 2733 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
11030, 109sralvec 32675 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
11192, 108, 14, 110syl3anc 1372 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
112 lveclmod 20717 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
113111, 112syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
114113adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐶 ∈ LMod)
115 eqid 2733 . . . . . . . . . . . . . . 15 (Base‘𝐶) = (Base‘𝐶)
116 eqid 2733 . . . . . . . . . . . . . . 15 (LBasis‘𝐶) = (LBasis‘𝐶)
117115, 116lbsss 20688 . . . . . . . . . . . . . 14 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
11847, 117syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (Base‘𝐶))
119118adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ⊆ (Base‘𝐶))
120 eqid 2733 . . . . . . . . . . . . . . . 16 (LSpan‘𝐶) = (LSpan‘𝐶)
121115, 116, 120islbs4 21387 . . . . . . . . . . . . . . 15 (𝑋 ∈ (LBasis‘𝐶) ↔ (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
12247, 121sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
123122simpld 496 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ (LIndS‘𝐶))
124123adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LIndS‘𝐶))
125 eqid 2733 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
126 eqid 2733 . . . . . . . . . . . . . 14 (Scalar‘𝐶) = (Scalar‘𝐶)
127 eqid 2733 . . . . . . . . . . . . . 14 ( ·𝑠𝐶) = ( ·𝑠𝐶)
128 eqid 2733 . . . . . . . . . . . . . 14 (0g𝐶) = (0g𝐶)
129 eqid 2733 . . . . . . . . . . . . . 14 (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
130115, 125, 126, 127, 128, 129islinds5 32480 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) → (𝑋 ∈ (LIndS‘𝐶) ↔ ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
131130biimpa 478 . . . . . . . . . . . 12 (((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) ∧ 𝑋 ∈ (LIndS‘𝐶)) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
132114, 119, 124, 131syl21anc 837 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
133106, 132, 55rspcdva 3614 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
13497, 133mpand 694 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
135134imp 408 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
13676, 78, 96, 135syl21anc 837 . . . . . . 7 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
1371, 136suppss 8179 . . . . . 6 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
13875, 137ssfid 9267 . . . . 5 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139 suppssdm 8162 . . . . . . . . . 10 (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140139, 1fssdm 6738 . . . . . . . . 9 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141140sselda 3983 . . . . . . . 8 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤𝑌)
142 eleq1w 2817 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝑗𝑌𝑤𝑌))
143142anbi2d 630 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝜑𝑗𝑌) ↔ (𝜑𝑤𝑌)))
144 fveq2 6892 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝐺𝑗) = (𝐺𝑤))
145144breq1d 5159 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶))))
146143, 145imbi12d 345 . . . . . . . . . 10 (𝑗 = 𝑤 → (((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))) ↔ ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))))
147146, 97chvarvv 2003 . . . . . . . . 9 ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))
148147fsuppimpd 9369 . . . . . . . 8 ((𝜑𝑤𝑌) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
149141, 148syldan 592 . . . . . . 7 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
150149ralrimiva 3147 . . . . . 6 (𝜑 → ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
151 iunfi 9340 . . . . . 6 (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
152138, 150, 151syl2anc 585 . . . . 5 (𝜑 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
153 xpfi 9317 . . . . 5 (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
154138, 152, 153syl2anc 585 . . . 4 (𝜑 → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
155 fveq2 6892 . . . . . . . . . 10 (𝑣 = 𝑗 → (𝐺𝑣) = (𝐺𝑗))
156155fveq1d 6894 . . . . . . . . 9 (𝑣 = 𝑗 → ((𝐺𝑣)‘𝑢) = ((𝐺𝑗)‘𝑢))
157156mpteq2dv 5251 . . . . . . . 8 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)))
158 fveq2 6892 . . . . . . . . 9 (𝑢 = 𝑖 → ((𝐺𝑗)‘𝑢) = ((𝐺𝑗)‘𝑖))
159158cbvmptv 5262 . . . . . . . 8 (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
160157, 159eqtrdi 2789 . . . . . . 7 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
161160cbvmptv 5262 . . . . . 6 (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = (𝑗𝑌 ↦ (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
162 fvexd 6907 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163 fvexd 6907 . . . . . 6 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ V)
16442, 161, 46, 47, 162, 163suppovss 31906 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
16510, 71subrg0 20326 . . . . . . . 8 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
16619, 165syl 17 . . . . . . 7 (𝜑 → (0g𝐸) = (0g𝐾))
16736fveq2d 6896 . . . . . . 7 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
168166, 167eqtr2d 2774 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g𝐸))
169168oveq2d 7425 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g𝐸)))
1701feqmptd 6961 . . . . . . . 8 (𝜑𝐺 = (𝑣𝑌 ↦ (𝐺𝑣)))
171 eleq1w 2817 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝑗𝑌𝑣𝑌))
172171anbi2d 630 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝜑𝑗𝑌) ↔ (𝜑𝑣𝑌)))
173 fveq2 6892 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝐺𝑗) = (𝐺𝑣))
174173feq1d 6703 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝐺𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺𝑣):𝑋⟶(Base‘𝐸)))
175172, 174imbi12d 345 . . . . . . . . . . 11 (𝑗 = 𝑣 → (((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))))
17610, 20ressbas2 17182 . . . . . . . . . . . . . . . 16 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
17722, 176syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉 = (Base‘𝐾))
17836fveq2d 6896 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
179177, 178eqtrd 2773 . . . . . . . . . . . . . 14 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
180179, 22eqsstrrd 4022 . . . . . . . . . . . . 13 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
181180adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
18256, 181fssd 6736 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸))
183175, 182chvarvv 2003 . . . . . . . . . 10 ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))
184183feqmptd 6961 . . . . . . . . 9 ((𝜑𝑣𝑌) → (𝐺𝑣) = (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))
185184mpteq2dva 5249 . . . . . . . 8 (𝜑 → (𝑣𝑌 ↦ (𝐺𝑣)) = (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))))
186170, 185eqtr2d 2774 . . . . . . 7 (𝜑 → (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = 𝐺)
187186oveq1d 7424 . . . . . 6 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188186fveq1d 6894 . . . . . . . 8 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) = (𝐺𝑤))
189188oveq1d 7424 . . . . . . 7 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
190187, 189iuneq12d 5026 . . . . . 6 (𝜑 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
191187, 190xpeq12d 5708 . . . . 5 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))) = ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
192164, 169, 1913sstr3d 4029 . . . 4 (𝜑 → (𝐻 supp (0g𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
193 suppssfifsupp 9378 . . . 4 (((𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ Fun 𝐻 ∧ (0g𝐸) ∈ (Base‘𝐸)) ∧ (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin ∧ (𝐻 supp (0g𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))) → 𝐻 finSupp (0g𝐸))
19452, 66, 73, 154, 192, 193syl32anc 1379 . . 3 (𝜑𝐻 finSupp (0g𝐸))
19537fveq2d 6896 . . . 4 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
196195, 168eqtr2d 2774 . . 3 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
197194, 196breqtrd 5175 . 2 (𝜑𝐻 finSupp (0g‘(Scalar‘𝐴)))
198 fedgmullem1.z . . 3 (𝜑𝑍 = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
19985, 67, 13, 15, 92, 46drgextgsum 32682 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
20047adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
20113adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202 subrgsubg 20325 . . . . . . . . . . . . 13 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203 subgsubm 19028 . . . . . . . . . . . . 13 (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204201, 202, 2033syl 18 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205113ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
20656ffvelcdmda 7087 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207118ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
208207, 61sseldd 3984 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
209115, 126, 127, 125lmodvscl 20489 . . . . . . . . . . . . . . 15 ((𝐶 ∈ LMod ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
210205, 206, 208, 209syl3anc 1372 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
21115, 20ressbas2 17182 . . . . . . . . . . . . . . . . 17 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
21288, 211syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑈 = (Base‘𝐹))
21331, 34srabase 20792 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
214212, 213eqtrd 2773 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝐶))
215214ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
216210, 215eleqtrrd 2837 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ 𝑈)
217216fmpttd 7115 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)):𝑋𝑈)
218200, 204, 217, 15gsumsubm 18716 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
219 eqid 2733 . . . . . . . . . . . . . . . . . 18 (.r𝐸) = (.r𝐸)
22015, 219ressmulr 17252 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
22113, 220syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐸) = (.r𝐹))
22231, 34sravsca 20800 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
223221, 222eqtr2d 2774 . . . . . . . . . . . . . . 15 (𝜑 → ( ·𝑠𝐶) = (.r𝐸))
224223ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐶) = (.r𝐸))
225224oveqd 7426 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))
226225mpteq2dva 5249 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))
227226oveq2d 7425 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))))
22830, 92, 14, 109, 108, 47drgextgsum 32682 . . . . . . . . . . . 12 (𝜑 → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
229228adantr 482 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
230218, 227, 2293eqtr3d 2781 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
231230oveq1d 7424 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
23269ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
233180ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
234233, 206sseldd 3984 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸))
235214, 88eqsstrrd 4022 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
236118, 235sstrd 3993 . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ (Base‘𝐸))
237236ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐸))
238237, 61sseldd 3984 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
239 eqid 2733 . . . . . . . . . . . . . . . . . 18 (Base‘𝐵) = (Base‘𝐵)
240 eqid 2733 . . . . . . . . . . . . . . . . . 18 (LBasis‘𝐵) = (LBasis‘𝐵)
241239, 240lbsss 20688 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
24246, 241syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ⊆ (Base‘𝐵))
24386, 88srabase 20792 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
244242, 243sseqtrrd 4024 . . . . . . . . . . . . . . 15 (𝜑𝑌 ⊆ (Base‘𝐸))
245244ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑌 ⊆ (Base‘𝐸))
246 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
247245, 246sseldd 3984 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
24820, 219ringass 20076 . . . . . . . . . . . . 13 ((𝐸 ∈ Ring ∧ (((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
249232, 234, 238, 247, 248syl13anc 1373 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
250249mpteq2dva 5249 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
251250oveq2d 7425 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
25269adantr 482 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
253242adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐵))
254243adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → (Base‘𝐸) = (Base‘𝐵))
255253, 254sseqtrrd 4024 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐸))
256 simpr 486 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑗𝑌)
257255, 256sseldd 3984 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
25820, 219ringcl 20073 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
259232, 234, 238, 258syl3anc 1372 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
260168breq2d 5161 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
261260adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
26297, 261mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g𝐸))
26320, 252, 200, 238, 182, 262rmfsupp2 32387 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
26420, 71, 219, 252, 200, 257, 259, 263gsummulc1 20128 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
265251, 264eqtr3d 2775 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
26683oveq1d 7424 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
267231, 265, 2663eqtr4rd 2784 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
26886, 88sravsca 20800 . . . . . . . . . 10 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
269268adantr 482 . . . . . . . . 9 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
270269oveqd 7426 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐿𝑗)( ·𝑠𝐵)𝑗))
271 fvexd 6907 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ V)
272 ovexd 7444 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
27342a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
274 fedgmullem.d . . . . . . . . . . . . . . 15 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
275274a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
27646, 47, 271, 272, 273, 275offval22 8074 . . . . . . . . . . . . 13 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
277276oveqd 7426 . . . . . . . . . . . 12 (𝜑 → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
278277ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
279 ovexd 7444 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V)
280 eqid 2733 . . . . . . . . . . . . 13 (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
281280ovmpt4g 7555 . . . . . . . . . . . 12 ((𝑗𝑌𝑖𝑋 ∧ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
282246, 61, 279, 281syl3anc 1372 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
283278, 282eqtr2d 2774 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) = (𝑗(𝐻f (.r𝐸)𝐷)𝑖))
284283mpteq2dva 5249 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))
285284oveq2d 7425 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
286267, 270, 2853eqtr3d 2781 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝐿𝑗)( ·𝑠𝐵)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
287286mpteq2dva 5249 . . . . . 6 (𝜑 → (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))))
288287oveq2d 7425 . . . . 5 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
289 ringcmn 20099 . . . . . . 7 (𝐸 ∈ Ring → 𝐸 ∈ CMnd)
29069, 289syl 17 . . . . . 6 (𝜑𝐸 ∈ CMnd)
29169adantr 482 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝐸 ∈ Ring)
29238, 180eqsstrd 4021 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
293292adantr 482 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
294 simprl 770 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘(Scalar‘𝐴)))
295293, 294sseldd 3984 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘𝐸))
296 simprr 772 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐴))
29712, 22srabase 20792 . . . . . . . . . 10 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
298297adantr 482 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘𝐸) = (Base‘𝐴))
299296, 298eleqtrrd 2837 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐸))
30020, 219ringcl 20073 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
301291, 295, 299, 300syl3anc 1372 . . . . . . 7 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
30220, 219ringcl 20073 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
303232, 238, 247, 302syl3anc 1372 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
304297ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
305303, 304eleqtrd 2836 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
306305anasss 468 . . . . . . . . 9 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
307306ralrimivva 3201 . . . . . . . 8 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
308274fmpo 8054 . . . . . . . 8 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
309307, 308sylib 217 . . . . . . 7 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310 inidm 4219 . . . . . . 7 ((𝑌 × 𝑋) ∩ (𝑌 × 𝑋)) = (𝑌 × 𝑋)
311301, 65, 309, 48, 48, 310off 7688 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐸))
31269adantr 482 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝐸 ∈ Ring)
313 simpr 486 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐴))
314297adantr 482 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → (Base‘𝐸) = (Base‘𝐴))
315313, 314eleqtrrd 2837 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐸))
31620, 219, 71ringlz 20107 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑢 ∈ (Base‘𝐸)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
317312, 315, 316syl2anc 585 . . . . . . 7 ((𝜑𝑢 ∈ (Base‘𝐴)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
31848, 73, 73, 65, 309, 194, 317offinsupp1 31952 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) finSupp (0g𝐸))
31920, 71, 290, 46, 47, 311, 318gsumxp 19844 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
32012, 22sravsca 20800 . . . . . . . 8 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
321320ofeqd 7672 . . . . . . 7 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
322321oveqd 7426 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝐻f ( ·𝑠𝐴)𝐷))
323322oveq2d 7425 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
324288, 319, 3233eqtr2rd 2780 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
325 ovexd 7444 . . . . 5 (𝜑 → (𝐻f ( ·𝑠𝐴)𝐷) ∈ V)
326 fedgmullem1.a . . . . . 6 (𝜑𝑍 ∈ (Base‘𝐴))
327326elfvexd 6931 . . . . 5 (𝜑𝐴 ∈ V)
32811, 325, 67, 327, 22gsumsra 32199 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
329324, 328eqtr3d 2775 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
330198, 199, 3293eqtr2d 2779 . 2 (𝜑𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
331197, 330jca 513 1 (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062  Vcvv 3475  cdif 3946  wss 3949  {csn 4629   ciun 4998   class class class wbr 5149  cmpt 5232   × cxp 5675  Fun wfun 6538  wf 6540  cfv 6544  (class class class)co 7409  cmpo 7411  f cof 7668   supp csupp 8146  m cmap 8820  Fincfn 8939   finSupp cfsupp 9361  Basecbs 17144  s cress 17173  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  0gc0g 17385   Σg cgsu 17386  SubMndcsubmnd 18670  Grpcgrp 18819  SubGrpcsubg 19000  CMndccmn 19648  Ringcrg 20056  SubRingcsubrg 20315  DivRingcdr 20357  LModclmod 20471  LSpanclspn 20582  LBasisclbs 20685  LVecclvec 20713  subringAlg csra 20781  LIndSclinds 21360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-hom 17221  df-cco 17222  df-0g 17387  df-gsum 17388  df-prds 17393  df-pws 17395  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-submnd 18672  df-grp 18822  df-minusg 18823  df-sbg 18824  df-mulg 18951  df-subg 19003  df-ghm 19090  df-cntz 19181  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-nzr 20292  df-subrg 20317  df-drng 20359  df-lmod 20473  df-lss 20543  df-lsp 20583  df-lmhm 20633  df-lbs 20686  df-lvec 20714  df-sra 20785  df-rgmod 20786  df-dsmm 21287  df-frlm 21302  df-uvc 21338  df-lindf 21361  df-linds 21362
This theorem is referenced by:  fedgmul  32716
  Copyright terms: Public domain W3C validator