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 33458
Description: Lemma for fedgmul 33460. (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 774 . . . . . . . . . . . . 13 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
3 simplr 767 . . . . . . . . . . . . 13 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
42, 3ffvelcdmd 7094 . . . . . . . . . . . 12 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5 elmapi 8868 . . . . . . . . . . . 12 ((𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
64, 5syl 17 . . . . . . . . . . 11 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
76anasss 465 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
8 simprr 771 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
97, 8ffvelcdmd 7094 . . . . . . . . 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 20549 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
1716biimpa 475 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1813, 14, 17syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1918simpld 493 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (SubRing‘𝐸))
20 eqid 2725 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2120subrgss 20523 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
2219, 21syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐸))
2312, 22srasca 21081 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
2410, 23eqtrid 2777 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐴))
2518simprd 494 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑈)
26 ressabs 17233 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2713, 25, 26syl2anc 582 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2815oveq1i 7429 . . . . . . . . . . . . . 14 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
2927, 28, 103eqtr4g 2790 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = 𝐾)
30 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
3130a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
32 eqid 2725 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
3332subrgss 20523 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
3414, 33syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3531, 34srasca 21081 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
3629, 35eqtr3d 2767 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐶))
3724, 36eqtr3d 2767 . . . . . . . . . . 11 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
3837fveq2d 6900 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
3938ad2antrr 724 . . . . . . . . 9 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
409, 39eleqtrrd 2828 . . . . . . . 8 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
4140ralrimivva 3190 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
42 fedgmullem.h . . . . . . . 8 𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
4342fmpo 8073 . . . . . . 7 (∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
4441, 43sylib 217 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45 fvexd 6911 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (Base‘(Scalar‘𝐴)) ∈ V)
46 fedgmullem.y . . . . . . . . 9 (𝜑𝑌 ∈ (LBasis‘𝐵))
47 fedgmullem.x . . . . . . . . 9 (𝜑𝑋 ∈ (LBasis‘𝐶))
4846, 47xpexd 7754 . . . . . . . 8 (𝜑 → (𝑌 × 𝑋) ∈ V)
4948adantr 479 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝑌 × 𝑋) ∈ V)
5045, 49elmapd 8859 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
5144, 50mpbird 256 . . . . 5 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
521, 51mpdan 685 . . . 4 (𝜑𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
53 simpl 481 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝜑)
5453adantr 479 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝜑)
551ffvelcdmda 7093 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5655, 5syl 17 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5756adantr 479 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5838feq3d 6710 . . . . . . . . . . 11 (𝜑 → ((𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)) ↔ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))))
5958biimpar 476 . . . . . . . . . 10 ((𝜑 ∧ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
6054, 57, 59syl2anc 582 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
61 simpr 483 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
6260, 61ffvelcdmd 7094 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6362ralrimiva 3135 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6463ralrimiva 3135 . . . . . 6 (𝜑 → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6564, 43sylib 217 . . . . 5 (𝜑𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
6665ffund 6727 . . . 4 (𝜑 → Fun 𝐻)
67 fedgmul.1 . . . . . 6 (𝜑𝐸 ∈ DivRing)
68 drngring 20643 . . . . . 6 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
6967, 68syl 17 . . . . 5 (𝜑𝐸 ∈ Ring)
70 ringgrp 20190 . . . . 5 (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71 eqid 2725 . . . . . 6 (0g𝐸) = (0g𝐸)
7220, 71grpidcl 18930 . . . . 5 (𝐸 ∈ Grp → (0g𝐸) ∈ (Base‘𝐸))
7369, 70, 723syl 18 . . . 4 (𝜑 → (0g𝐸) ∈ (Base‘𝐸))
74 fedgmullem1.1 . . . . . . 7 (𝜑𝐿 finSupp (0g‘(Scalar‘𝐵)))
7574fsuppimpd 9395 . . . . . 6 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ∈ Fin)
76 simpl 481 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝜑)
77 simpr 483 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵)))))
7877eldifad 3956 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗𝑌)
79 fedgmullem1.l . . . . . . . . . 10 (𝜑𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
80 ssidd 4000 . . . . . . . . . 10 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
81 fvexd 6911 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
8279, 80, 46, 81suppssr 8201 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿𝑗) = (0g‘(Scalar‘𝐵)))
83 fedgmullem1.3 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
8478, 83syldan 589 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
85 fedgmul.b . . . . . . . . . . . . . . 15 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
8685a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
8720subrgss 20523 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
8986, 88srasca 21081 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
9015, 89eqtrid 2777 . . . . . . . . . . . 12 (𝜑𝐹 = (Scalar‘𝐵))
9190fveq2d 6900 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐵)))
92 fedgmul.2 . . . . . . . . . . . 12 (𝜑𝐹 ∈ DivRing)
9330, 92, 14drgext0g 33420 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g𝐶))
9491, 93eqtr3d 2767 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9594adantr 479 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9682, 84, 953eqtr3d 2773 . . . . . . . 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 6895 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝐺𝑗) → (𝑔𝑖) = ((𝐺𝑗)‘𝑖))
10099oveq1d 7434 . . . . . . . . . . . . . . . 16 (𝑔 = (𝐺𝑗) → ((𝑔𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))
101100mpteq2dv 5251 . . . . . . . . . . . . . . 15 (𝑔 = (𝐺𝑗) → (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
102101oveq2d 7435 . . . . . . . . . . . . . 14 (𝑔 = (𝐺𝑗) → (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
103102eqeq1d 2727 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → ((𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) ↔ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)))
10498, 103anbi12d 630 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → ((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) ↔ ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))))
105 eqeq1 2729 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → (𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}) ↔ (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
106104, 105imbi12d 343 . . . . . . . . . . 11 (𝑔 = (𝐺𝑗) → (((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})) ↔ (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
107 fedgmul.3 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ DivRing)
10829, 107eqeltrd 2825 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
109 eqid 2725 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
11030, 109sralvec 33416 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
11192, 108, 14, 110syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
112 lveclmod 21003 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
113111, 112syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
114113adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐶 ∈ LMod)
115 eqid 2725 . . . . . . . . . . . . . . 15 (Base‘𝐶) = (Base‘𝐶)
116 eqid 2725 . . . . . . . . . . . . . . 15 (LBasis‘𝐶) = (LBasis‘𝐶)
117115, 116lbsss 20974 . . . . . . . . . . . . . 14 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
11847, 117syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (Base‘𝐶))
119118adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ⊆ (Base‘𝐶))
120 eqid 2725 . . . . . . . . . . . . . . . 16 (LSpan‘𝐶) = (LSpan‘𝐶)
121115, 116, 120islbs4 21783 . . . . . . . . . . . . . . 15 (𝑋 ∈ (LBasis‘𝐶) ↔ (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
12247, 121sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
123122simpld 493 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ (LIndS‘𝐶))
124123adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LIndS‘𝐶))
125 eqid 2725 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
126 eqid 2725 . . . . . . . . . . . . . 14 (Scalar‘𝐶) = (Scalar‘𝐶)
127 eqid 2725 . . . . . . . . . . . . . 14 ( ·𝑠𝐶) = ( ·𝑠𝐶)
128 eqid 2725 . . . . . . . . . . . . . 14 (0g𝐶) = (0g𝐶)
129 eqid 2725 . . . . . . . . . . . . . 14 (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
130115, 125, 126, 127, 128, 129islinds5 33178 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) → (𝑋 ∈ (LIndS‘𝐶) ↔ ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
131130biimpa 475 . . . . . . . . . . . 12 (((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) ∧ 𝑋 ∈ (LIndS‘𝐶)) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
132114, 119, 124, 131syl21anc 836 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
133106, 132, 55rspcdva 3607 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
13497, 133mpand 693 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
135134imp 405 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
13676, 78, 96, 135syl21anc 836 . . . . . . 7 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
1371, 136suppss 8199 . . . . . 6 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
13875, 137ssfid 9292 . . . . 5 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139 suppssdm 8182 . . . . . . . . . 10 (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140139, 1fssdm 6742 . . . . . . . . 9 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141140sselda 3976 . . . . . . . 8 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤𝑌)
142 eleq1w 2808 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝑗𝑌𝑤𝑌))
143142anbi2d 628 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝜑𝑗𝑌) ↔ (𝜑𝑤𝑌)))
144 fveq2 6896 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝐺𝑗) = (𝐺𝑤))
145144breq1d 5159 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶))))
146143, 145imbi12d 343 . . . . . . . . . 10 (𝑗 = 𝑤 → (((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))) ↔ ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))))
147146, 97chvarvv 1994 . . . . . . . . 9 ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))
148147fsuppimpd 9395 . . . . . . . 8 ((𝜑𝑤𝑌) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
149141, 148syldan 589 . . . . . . 7 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
150149ralrimiva 3135 . . . . . 6 (𝜑 → ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
151 iunfi 9366 . . . . . 6 (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
152138, 150, 151syl2anc 582 . . . . 5 (𝜑 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
153 xpfi 9343 . . . . 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 582 . . . 4 (𝜑 → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
155 fveq2 6896 . . . . . . . . . 10 (𝑣 = 𝑗 → (𝐺𝑣) = (𝐺𝑗))
156155fveq1d 6898 . . . . . . . . 9 (𝑣 = 𝑗 → ((𝐺𝑣)‘𝑢) = ((𝐺𝑗)‘𝑢))
157156mpteq2dv 5251 . . . . . . . 8 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)))
158 fveq2 6896 . . . . . . . . 9 (𝑢 = 𝑖 → ((𝐺𝑗)‘𝑢) = ((𝐺𝑗)‘𝑖))
159158cbvmptv 5262 . . . . . . . 8 (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
160157, 159eqtrdi 2781 . . . . . . 7 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
161160cbvmptv 5262 . . . . . 6 (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = (𝑗𝑌 ↦ (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
162 fvexd 6911 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163 fvexd 6911 . . . . . 6 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ V)
16442, 161, 46, 47, 162, 163suppovss 32547 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
16510, 71subrg0 20530 . . . . . . . 8 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
16619, 165syl 17 . . . . . . 7 (𝜑 → (0g𝐸) = (0g𝐾))
16736fveq2d 6900 . . . . . . 7 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
168166, 167eqtr2d 2766 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g𝐸))
169168oveq2d 7435 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g𝐸)))
1701feqmptd 6966 . . . . . . . 8 (𝜑𝐺 = (𝑣𝑌 ↦ (𝐺𝑣)))
171 eleq1w 2808 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝑗𝑌𝑣𝑌))
172171anbi2d 628 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝜑𝑗𝑌) ↔ (𝜑𝑣𝑌)))
173 fveq2 6896 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝐺𝑗) = (𝐺𝑣))
174173feq1d 6708 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝐺𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺𝑣):𝑋⟶(Base‘𝐸)))
175172, 174imbi12d 343 . . . . . . . . . . 11 (𝑗 = 𝑣 → (((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))))
17610, 20ressbas2 17221 . . . . . . . . . . . . . . . 16 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
17722, 176syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉 = (Base‘𝐾))
17836fveq2d 6900 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
179177, 178eqtrd 2765 . . . . . . . . . . . . . 14 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
180179, 22eqsstrrd 4016 . . . . . . . . . . . . 13 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
181180adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
18256, 181fssd 6740 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸))
183175, 182chvarvv 1994 . . . . . . . . . 10 ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))
184183feqmptd 6966 . . . . . . . . 9 ((𝜑𝑣𝑌) → (𝐺𝑣) = (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))
185184mpteq2dva 5249 . . . . . . . 8 (𝜑 → (𝑣𝑌 ↦ (𝐺𝑣)) = (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))))
186170, 185eqtr2d 2766 . . . . . . 7 (𝜑 → (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = 𝐺)
187186oveq1d 7434 . . . . . 6 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188186fveq1d 6898 . . . . . . . 8 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) = (𝐺𝑤))
189188oveq1d 7434 . . . . . . 7 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
190187, 189iuneq12d 5025 . . . . . 6 (𝜑 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
191187, 190xpeq12d 5709 . . . . 5 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))) = ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
192164, 169, 1913sstr3d 4023 . . . 4 (𝜑 → (𝐻 supp (0g𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
193 suppssfifsupp 9405 . . . 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 1375 . . 3 (𝜑𝐻 finSupp (0g𝐸))
19537fveq2d 6900 . . . 4 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
196195, 168eqtr2d 2766 . . 3 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
197194, 196breqtrd 5175 . 2 (𝜑𝐻 finSupp (0g‘(Scalar‘𝐴)))
198 fedgmullem1.z . . 3 (𝜑𝑍 = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
19985, 67, 13, 15, 92, 46drgextgsum 33425 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
20047adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
20113adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202 subrgsubg 20528 . . . . . . . . . . . . 13 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203 subgsubm 19111 . . . . . . . . . . . . 13 (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204201, 202, 2033syl 18 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205113ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
20656ffvelcdmda 7093 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207118ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
208207, 61sseldd 3977 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
209115, 126, 127, 125lmodvscl 20773 . . . . . . . . . . . . . . 15 ((𝐶 ∈ LMod ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
210205, 206, 208, 209syl3anc 1368 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
21115, 20ressbas2 17221 . . . . . . . . . . . . . . . . 17 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
21288, 211syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑈 = (Base‘𝐹))
21331, 34srabase 21075 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
214212, 213eqtrd 2765 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝐶))
215214ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
216210, 215eleqtrrd 2828 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ 𝑈)
217216fmpttd 7124 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)):𝑋𝑈)
218200, 204, 217, 15gsumsubm 18795 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
219 eqid 2725 . . . . . . . . . . . . . . . . . 18 (.r𝐸) = (.r𝐸)
22015, 219ressmulr 17291 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
22113, 220syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐸) = (.r𝐹))
22231, 34sravsca 21083 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
223221, 222eqtr2d 2766 . . . . . . . . . . . . . . 15 (𝜑 → ( ·𝑠𝐶) = (.r𝐸))
224223ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐶) = (.r𝐸))
225224oveqd 7436 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))
226225mpteq2dva 5249 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))
227226oveq2d 7435 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))))
22830, 92, 14, 109, 108, 47drgextgsum 33425 . . . . . . . . . . . 12 (𝜑 → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
229228adantr 479 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
230218, 227, 2293eqtr3d 2773 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
231230oveq1d 7434 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
23269ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
233180ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
234233, 206sseldd 3977 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸))
235214, 88eqsstrrd 4016 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
236118, 235sstrd 3987 . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ (Base‘𝐸))
237236ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐸))
238237, 61sseldd 3977 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
239 eqid 2725 . . . . . . . . . . . . . . . . . 18 (Base‘𝐵) = (Base‘𝐵)
240 eqid 2725 . . . . . . . . . . . . . . . . . 18 (LBasis‘𝐵) = (LBasis‘𝐵)
241239, 240lbsss 20974 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
24246, 241syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ⊆ (Base‘𝐵))
24386, 88srabase 21075 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
244242, 243sseqtrrd 4018 . . . . . . . . . . . . . . 15 (𝜑𝑌 ⊆ (Base‘𝐸))
245244ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑌 ⊆ (Base‘𝐸))
246 simplr 767 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
247245, 246sseldd 3977 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
24820, 219ringass 20205 . . . . . . . . . . . . 13 ((𝐸 ∈ Ring ∧ (((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
249232, 234, 238, 247, 248syl13anc 1369 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
250249mpteq2dva 5249 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
251250oveq2d 7435 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
25269adantr 479 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
253242adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐵))
254243adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → (Base‘𝐸) = (Base‘𝐵))
255253, 254sseqtrrd 4018 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐸))
256 simpr 483 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑗𝑌)
257255, 256sseldd 3977 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
25820, 219ringcl 20202 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
259232, 234, 238, 258syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
260168breq2d 5161 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
261260adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
26297, 261mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g𝐸))
26320, 252, 200, 238, 182, 262rmfsupp2 33038 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
26420, 71, 219, 252, 200, 257, 259, 263gsummulc1 20264 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
265251, 264eqtr3d 2767 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
26683oveq1d 7434 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
267231, 265, 2663eqtr4rd 2776 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
26886, 88sravsca 21083 . . . . . . . . . 10 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
269268adantr 479 . . . . . . . . 9 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
270269oveqd 7436 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐿𝑗)( ·𝑠𝐵)𝑗))
271 fvexd 6911 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ V)
272 ovexd 7454 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
27342a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
274 fedgmullem.d . . . . . . . . . . . . . . 15 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
275274a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
27646, 47, 271, 272, 273, 275offval22 8093 . . . . . . . . . . . . 13 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
277276oveqd 7436 . . . . . . . . . . . 12 (𝜑 → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
278277ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
279 ovexd 7454 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V)
280 eqid 2725 . . . . . . . . . . . . 13 (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
281280ovmpt4g 7568 . . . . . . . . . . . 12 ((𝑗𝑌𝑖𝑋 ∧ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
282246, 61, 279, 281syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
283278, 282eqtr2d 2766 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) = (𝑗(𝐻f (.r𝐸)𝐷)𝑖))
284283mpteq2dva 5249 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))
285284oveq2d 7435 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
286267, 270, 2853eqtr3d 2773 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝐿𝑗)( ·𝑠𝐵)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
287286mpteq2dva 5249 . . . . . 6 (𝜑 → (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))))
288287oveq2d 7435 . . . . 5 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
289 ringcmn 20230 . . . . . . 7 (𝐸 ∈ Ring → 𝐸 ∈ CMnd)
29069, 289syl 17 . . . . . 6 (𝜑𝐸 ∈ CMnd)
29169adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝐸 ∈ Ring)
29238, 180eqsstrd 4015 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
293292adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
294 simprl 769 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘(Scalar‘𝐴)))
295293, 294sseldd 3977 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘𝐸))
296 simprr 771 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐴))
29712, 22srabase 21075 . . . . . . . . . 10 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
298297adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘𝐸) = (Base‘𝐴))
299296, 298eleqtrrd 2828 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐸))
30020, 219ringcl 20202 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
301291, 295, 299, 300syl3anc 1368 . . . . . . 7 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
30220, 219ringcl 20202 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
303232, 238, 247, 302syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
304297ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
305303, 304eleqtrd 2827 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
306305anasss 465 . . . . . . . . 9 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
307306ralrimivva 3190 . . . . . . . 8 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
308274fmpo 8073 . . . . . . . 8 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
309307, 308sylib 217 . . . . . . 7 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310 inidm 4217 . . . . . . 7 ((𝑌 × 𝑋) ∩ (𝑌 × 𝑋)) = (𝑌 × 𝑋)
311301, 65, 309, 48, 48, 310off 7703 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐸))
31269adantr 479 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝐸 ∈ Ring)
313 simpr 483 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐴))
314297adantr 479 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → (Base‘𝐸) = (Base‘𝐴))
315313, 314eleqtrrd 2828 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐸))
31620, 219, 71ringlz 20241 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑢 ∈ (Base‘𝐸)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
317312, 315, 316syl2anc 582 . . . . . . 7 ((𝜑𝑢 ∈ (Base‘𝐴)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
31848, 73, 73, 65, 309, 194, 317offinsupp1 32591 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) finSupp (0g𝐸))
31920, 71, 290, 46, 47, 311, 318gsumxp 19943 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
32012, 22sravsca 21083 . . . . . . . 8 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
321320ofeqd 7687 . . . . . . 7 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
322321oveqd 7436 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝐻f ( ·𝑠𝐴)𝐷))
323322oveq2d 7435 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
324288, 319, 3233eqtr2rd 2772 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
325 ovexd 7454 . . . . 5 (𝜑 → (𝐻f ( ·𝑠𝐴)𝐷) ∈ V)
326 fedgmullem1.a . . . . . 6 (𝜑𝑍 ∈ (Base‘𝐴))
327326elfvexd 6935 . . . . 5 (𝜑𝐴 ∈ V)
32811, 325, 67, 327, 22gsumsra 32851 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
329324, 328eqtr3d 2767 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
330198, 199, 3293eqtr2d 2771 . 2 (𝜑𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
331197, 330jca 510 1 (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  Vcvv 3461  cdif 3941  wss 3944  {csn 4630   ciun 4997   class class class wbr 5149  cmpt 5232   × cxp 5676  Fun wfun 6543  wf 6545  cfv 6549  (class class class)co 7419  cmpo 7421  f cof 7683   supp csupp 8165  m cmap 8845  Fincfn 8964   finSupp cfsupp 9387  Basecbs 17183  s cress 17212  .rcmulr 17237  Scalarcsca 17239   ·𝑠 cvsca 17240  0gc0g 17424   Σg cgsu 17425  SubMndcsubmnd 18742  Grpcgrp 18898  SubGrpcsubg 19083  CMndccmn 19747  Ringcrg 20185  SubRingcsubrg 20518  DivRingcdr 20636  LModclmod 20755  LSpanclspn 20867  LBasisclbs 20971  LVecclvec 20999  subringAlg csra 21068  LIndSclinds 21756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-sup 9467  df-oi 9535  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12506  df-z 12592  df-dec 12711  df-uz 12856  df-fz 13520  df-fzo 13663  df-seq 14003  df-hash 14326  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-sca 17252  df-vsca 17253  df-ip 17254  df-tset 17255  df-ple 17256  df-ds 17258  df-hom 17260  df-cco 17261  df-0g 17426  df-gsum 17427  df-prds 17432  df-pws 17434  df-mre 17569  df-mrc 17570  df-acs 17572  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18743  df-submnd 18744  df-grp 18901  df-minusg 18902  df-sbg 18903  df-mulg 19032  df-subg 19086  df-ghm 19176  df-cntz 19280  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-nzr 20464  df-subrg 20520  df-drng 20638  df-lmod 20757  df-lss 20828  df-lsp 20868  df-lmhm 20919  df-lbs 20972  df-lvec 21000  df-sra 21070  df-rgmod 21071  df-dsmm 21683  df-frlm 21698  df-uvc 21734  df-lindf 21757  df-linds 21758
This theorem is referenced by:  fedgmul  33460
  Copyright terms: Public domain W3C validator