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 33680
Description: Lemma for fedgmul 33682. (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 776 . . . . . . . . . . . . 13 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
3 simplr 769 . . . . . . . . . . . . 13 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
42, 3ffvelcdmd 7105 . . . . . . . . . . . 12 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5 elmapi 8889 . . . . . . . . . . . 12 ((𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
64, 5syl 17 . . . . . . . . . . 11 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
76anasss 466 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
8 simprr 773 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
97, 8ffvelcdmd 7105 . . . . . . . . 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 20598 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
1716biimpa 476 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1813, 14, 17syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1918simpld 494 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (SubRing‘𝐸))
20 eqid 2737 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2120subrgss 20572 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
2219, 21syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐸))
2312, 22srasca 21183 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
2410, 23eqtrid 2789 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐴))
2518simprd 495 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑈)
26 ressabs 17294 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2713, 25, 26syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2815oveq1i 7441 . . . . . . . . . . . . . 14 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
2927, 28, 103eqtr4g 2802 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = 𝐾)
30 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
3130a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
32 eqid 2737 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
3332subrgss 20572 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
3414, 33syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3531, 34srasca 21183 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
3629, 35eqtr3d 2779 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐶))
3724, 36eqtr3d 2779 . . . . . . . . . . 11 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
3837fveq2d 6910 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
3938ad2antrr 726 . . . . . . . . 9 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
409, 39eleqtrrd 2844 . . . . . . . 8 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
4140ralrimivva 3202 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
42 fedgmullem.h . . . . . . . 8 𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
4342fmpo 8093 . . . . . . 7 (∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
4441, 43sylib 218 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45 fvexd 6921 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (Base‘(Scalar‘𝐴)) ∈ V)
46 fedgmullem.y . . . . . . . . 9 (𝜑𝑌 ∈ (LBasis‘𝐵))
47 fedgmullem.x . . . . . . . . 9 (𝜑𝑋 ∈ (LBasis‘𝐶))
4846, 47xpexd 7771 . . . . . . . 8 (𝜑 → (𝑌 × 𝑋) ∈ V)
4948adantr 480 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝑌 × 𝑋) ∈ V)
5045, 49elmapd 8880 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
5144, 50mpbird 257 . . . . 5 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
521, 51mpdan 687 . . . 4 (𝜑𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
53 simpl 482 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝜑)
5453adantr 480 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝜑)
551ffvelcdmda 7104 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5655, 5syl 17 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5756adantr 480 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5838feq3d 6723 . . . . . . . . . . 11 (𝜑 → ((𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)) ↔ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))))
5958biimpar 477 . . . . . . . . . 10 ((𝜑 ∧ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
6054, 57, 59syl2anc 584 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
61 simpr 484 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
6260, 61ffvelcdmd 7105 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6362ralrimiva 3146 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6463ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6564, 43sylib 218 . . . . 5 (𝜑𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
6665ffund 6740 . . . 4 (𝜑 → Fun 𝐻)
67 fedgmul.1 . . . . . 6 (𝜑𝐸 ∈ DivRing)
68 drngring 20736 . . . . . 6 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
6967, 68syl 17 . . . . 5 (𝜑𝐸 ∈ Ring)
70 ringgrp 20235 . . . . 5 (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71 eqid 2737 . . . . . 6 (0g𝐸) = (0g𝐸)
7220, 71grpidcl 18983 . . . . 5 (𝐸 ∈ Grp → (0g𝐸) ∈ (Base‘𝐸))
7369, 70, 723syl 18 . . . 4 (𝜑 → (0g𝐸) ∈ (Base‘𝐸))
74 fedgmullem1.1 . . . . . . 7 (𝜑𝐿 finSupp (0g‘(Scalar‘𝐵)))
7574fsuppimpd 9409 . . . . . 6 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ∈ Fin)
76 simpl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝜑)
77 simpr 484 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵)))))
7877eldifad 3963 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗𝑌)
79 fedgmullem1.l . . . . . . . . . 10 (𝜑𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
80 ssidd 4007 . . . . . . . . . 10 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
81 fvexd 6921 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
8279, 80, 46, 81suppssr 8220 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿𝑗) = (0g‘(Scalar‘𝐵)))
83 fedgmullem1.3 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
8478, 83syldan 591 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿𝑗) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
85 fedgmul.b . . . . . . . . . . . . . . 15 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
8685a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
8720subrgss 20572 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
8986, 88srasca 21183 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
9015, 89eqtrid 2789 . . . . . . . . . . . 12 (𝜑𝐹 = (Scalar‘𝐵))
9190fveq2d 6910 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐵)))
92 fedgmul.2 . . . . . . . . . . . 12 (𝜑𝐹 ∈ DivRing)
9330, 92, 14drgext0g 33640 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g𝐶))
9491, 93eqtr3d 2779 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9594adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9682, 84, 953eqtr3d 2785 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))
97 fedgmullem1.2 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)))
98 breq1 5146 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → (𝑔 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))))
99 fveq1 6905 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝐺𝑗) → (𝑔𝑖) = ((𝐺𝑗)‘𝑖))
10099oveq1d 7446 . . . . . . . . . . . . . . . 16 (𝑔 = (𝐺𝑗) → ((𝑔𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))
101100mpteq2dv 5244 . . . . . . . . . . . . . . 15 (𝑔 = (𝐺𝑗) → (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
102101oveq2d 7447 . . . . . . . . . . . . . 14 (𝑔 = (𝐺𝑗) → (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
103102eqeq1d 2739 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → ((𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) ↔ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)))
10498, 103anbi12d 632 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → ((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) ↔ ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))))
105 eqeq1 2741 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → (𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}) ↔ (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
106104, 105imbi12d 344 . . . . . . . . . . 11 (𝑔 = (𝐺𝑗) → (((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})) ↔ (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
107 fedgmul.3 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ DivRing)
10829, 107eqeltrd 2841 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
109 eqid 2737 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
11030, 109sralvec 33636 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
11192, 108, 14, 110syl3anc 1373 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
112 lveclmod 21105 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
113111, 112syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
114113adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐶 ∈ LMod)
115 eqid 2737 . . . . . . . . . . . . . . 15 (Base‘𝐶) = (Base‘𝐶)
116 eqid 2737 . . . . . . . . . . . . . . 15 (LBasis‘𝐶) = (LBasis‘𝐶)
117115, 116lbsss 21076 . . . . . . . . . . . . . 14 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
11847, 117syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (Base‘𝐶))
119118adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ⊆ (Base‘𝐶))
120 eqid 2737 . . . . . . . . . . . . . . . 16 (LSpan‘𝐶) = (LSpan‘𝐶)
121115, 116, 120islbs4 21852 . . . . . . . . . . . . . . 15 (𝑋 ∈ (LBasis‘𝐶) ↔ (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
12247, 121sylib 218 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
123122simpld 494 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ (LIndS‘𝐶))
124123adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LIndS‘𝐶))
125 eqid 2737 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
126 eqid 2737 . . . . . . . . . . . . . 14 (Scalar‘𝐶) = (Scalar‘𝐶)
127 eqid 2737 . . . . . . . . . . . . . 14 ( ·𝑠𝐶) = ( ·𝑠𝐶)
128 eqid 2737 . . . . . . . . . . . . . 14 (0g𝐶) = (0g𝐶)
129 eqid 2737 . . . . . . . . . . . . . 14 (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
130115, 125, 126, 127, 128, 129islinds5 33395 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) → (𝑋 ∈ (LIndS‘𝐶) ↔ ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
131130biimpa 476 . . . . . . . . . . . 12 (((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) ∧ 𝑋 ∈ (LIndS‘𝐶)) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
132114, 119, 124, 131syl21anc 838 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
133106, 132, 55rspcdva 3623 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
13497, 133mpand 695 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
135134imp 406 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
13676, 78, 96, 135syl21anc 838 . . . . . . 7 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
1371, 136suppss 8219 . . . . . 6 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
13875, 137ssfid 9301 . . . . 5 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139 suppssdm 8202 . . . . . . . . . 10 (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140139, 1fssdm 6755 . . . . . . . . 9 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141140sselda 3983 . . . . . . . 8 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤𝑌)
142 eleq1w 2824 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝑗𝑌𝑤𝑌))
143142anbi2d 630 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝜑𝑗𝑌) ↔ (𝜑𝑤𝑌)))
144 fveq2 6906 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝐺𝑗) = (𝐺𝑤))
145144breq1d 5153 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶))))
146143, 145imbi12d 344 . . . . . . . . . 10 (𝑗 = 𝑤 → (((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))) ↔ ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))))
147146, 97chvarvv 1998 . . . . . . . . 9 ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))
148147fsuppimpd 9409 . . . . . . . 8 ((𝜑𝑤𝑌) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
149141, 148syldan 591 . . . . . . 7 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
150149ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
151 iunfi 9383 . . . . . 6 (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
152138, 150, 151syl2anc 584 . . . . 5 (𝜑 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
153 xpfi 9358 . . . . 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 584 . . . 4 (𝜑 → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
155 fveq2 6906 . . . . . . . . . 10 (𝑣 = 𝑗 → (𝐺𝑣) = (𝐺𝑗))
156155fveq1d 6908 . . . . . . . . 9 (𝑣 = 𝑗 → ((𝐺𝑣)‘𝑢) = ((𝐺𝑗)‘𝑢))
157156mpteq2dv 5244 . . . . . . . 8 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)))
158 fveq2 6906 . . . . . . . . 9 (𝑢 = 𝑖 → ((𝐺𝑗)‘𝑢) = ((𝐺𝑗)‘𝑖))
159158cbvmptv 5255 . . . . . . . 8 (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
160157, 159eqtrdi 2793 . . . . . . 7 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
161160cbvmptv 5255 . . . . . 6 (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = (𝑗𝑌 ↦ (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
162 fvexd 6921 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163 fvexd 6921 . . . . . 6 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ V)
16442, 161, 46, 47, 162, 163suppovss 32690 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
16510, 71subrg0 20579 . . . . . . . 8 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
16619, 165syl 17 . . . . . . 7 (𝜑 → (0g𝐸) = (0g𝐾))
16736fveq2d 6910 . . . . . . 7 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
168166, 167eqtr2d 2778 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g𝐸))
169168oveq2d 7447 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g𝐸)))
1701feqmptd 6977 . . . . . . . 8 (𝜑𝐺 = (𝑣𝑌 ↦ (𝐺𝑣)))
171 eleq1w 2824 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝑗𝑌𝑣𝑌))
172171anbi2d 630 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝜑𝑗𝑌) ↔ (𝜑𝑣𝑌)))
173 fveq2 6906 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝐺𝑗) = (𝐺𝑣))
174173feq1d 6720 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝐺𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺𝑣):𝑋⟶(Base‘𝐸)))
175172, 174imbi12d 344 . . . . . . . . . . 11 (𝑗 = 𝑣 → (((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))))
17610, 20ressbas2 17283 . . . . . . . . . . . . . . . 16 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
17722, 176syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉 = (Base‘𝐾))
17836fveq2d 6910 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
179177, 178eqtrd 2777 . . . . . . . . . . . . . 14 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
180179, 22eqsstrrd 4019 . . . . . . . . . . . . 13 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
181180adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
18256, 181fssd 6753 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸))
183175, 182chvarvv 1998 . . . . . . . . . 10 ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))
184183feqmptd 6977 . . . . . . . . 9 ((𝜑𝑣𝑌) → (𝐺𝑣) = (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))
185184mpteq2dva 5242 . . . . . . . 8 (𝜑 → (𝑣𝑌 ↦ (𝐺𝑣)) = (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))))
186170, 185eqtr2d 2778 . . . . . . 7 (𝜑 → (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = 𝐺)
187186oveq1d 7446 . . . . . 6 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188186fveq1d 6908 . . . . . . . 8 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) = (𝐺𝑤))
189188oveq1d 7446 . . . . . . 7 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
190187, 189iuneq12d 5021 . . . . . 6 (𝜑 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
191187, 190xpeq12d 5716 . . . . 5 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))) = ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
192164, 169, 1913sstr3d 4038 . . . 4 (𝜑 → (𝐻 supp (0g𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
193 suppssfifsupp 9420 . . . 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 1380 . . 3 (𝜑𝐻 finSupp (0g𝐸))
19537fveq2d 6910 . . . 4 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
196195, 168eqtr2d 2778 . . 3 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
197194, 196breqtrd 5169 . 2 (𝜑𝐻 finSupp (0g‘(Scalar‘𝐴)))
198 fedgmullem1.z . . 3 (𝜑𝑍 = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
19985, 67, 13, 15, 92, 46drgextgsum 33645 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
20047adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
20113adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202 subrgsubg 20577 . . . . . . . . . . . . 13 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203 subgsubm 19166 . . . . . . . . . . . . 13 (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204201, 202, 2033syl 18 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205113ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
20656ffvelcdmda 7104 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207118ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
208207, 61sseldd 3984 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
209115, 126, 127, 125lmodvscl 20876 . . . . . . . . . . . . . . 15 ((𝐶 ∈ LMod ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
210205, 206, 208, 209syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
21115, 20ressbas2 17283 . . . . . . . . . . . . . . . . 17 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
21288, 211syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑈 = (Base‘𝐹))
21331, 34srabase 21177 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
214212, 213eqtrd 2777 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝐶))
215214ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
216210, 215eleqtrrd 2844 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ 𝑈)
217216fmpttd 7135 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)):𝑋𝑈)
218200, 204, 217, 15gsumsubm 18848 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
219 eqid 2737 . . . . . . . . . . . . . . . . . 18 (.r𝐸) = (.r𝐸)
22015, 219ressmulr 17351 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
22113, 220syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐸) = (.r𝐹))
22231, 34sravsca 21185 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
223221, 222eqtr2d 2778 . . . . . . . . . . . . . . 15 (𝜑 → ( ·𝑠𝐶) = (.r𝐸))
224223ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐶) = (.r𝐸))
225224oveqd 7448 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))
226225mpteq2dva 5242 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))
227226oveq2d 7447 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))))
22830, 92, 14, 109, 108, 47drgextgsum 33645 . . . . . . . . . . . 12 (𝜑 → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
229228adantr 480 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
230218, 227, 2293eqtr3d 2785 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
231230oveq1d 7446 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
23269ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
233180ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
234233, 206sseldd 3984 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸))
235214, 88eqsstrrd 4019 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
236118, 235sstrd 3994 . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ (Base‘𝐸))
237236ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐸))
238237, 61sseldd 3984 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
239 eqid 2737 . . . . . . . . . . . . . . . . . 18 (Base‘𝐵) = (Base‘𝐵)
240 eqid 2737 . . . . . . . . . . . . . . . . . 18 (LBasis‘𝐵) = (LBasis‘𝐵)
241239, 240lbsss 21076 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
24246, 241syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ⊆ (Base‘𝐵))
24386, 88srabase 21177 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
244242, 243sseqtrrd 4021 . . . . . . . . . . . . . . 15 (𝜑𝑌 ⊆ (Base‘𝐸))
245244ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑌 ⊆ (Base‘𝐸))
246 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
247245, 246sseldd 3984 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
24820, 219ringass 20250 . . . . . . . . . . . . 13 ((𝐸 ∈ Ring ∧ (((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
249232, 234, 238, 247, 248syl13anc 1374 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
250249mpteq2dva 5242 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
251250oveq2d 7447 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
25269adantr 480 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
253242adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐵))
254243adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → (Base‘𝐸) = (Base‘𝐵))
255253, 254sseqtrrd 4021 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐸))
256 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑗𝑌)
257255, 256sseldd 3984 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
25820, 219ringcl 20247 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
259232, 234, 238, 258syl3anc 1373 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
260168breq2d 5155 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
261260adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
26297, 261mpbid 232 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g𝐸))
26320, 252, 200, 238, 182, 262rmfsupp2 33242 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
26420, 71, 219, 252, 200, 257, 259, 263gsummulc1 20313 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
265251, 264eqtr3d 2779 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
26683oveq1d 7446 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
267231, 265, 2663eqtr4rd 2788 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
26886, 88sravsca 21185 . . . . . . . . . 10 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
269268adantr 480 . . . . . . . . 9 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
270269oveqd 7448 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐿𝑗)( ·𝑠𝐵)𝑗))
271 fvexd 6921 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ V)
272 ovexd 7466 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
27342a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
274 fedgmullem.d . . . . . . . . . . . . . . 15 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
275274a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
27646, 47, 271, 272, 273, 275offval22 8113 . . . . . . . . . . . . 13 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
277276oveqd 7448 . . . . . . . . . . . 12 (𝜑 → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
278277ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
279 ovexd 7466 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V)
280 eqid 2737 . . . . . . . . . . . . 13 (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
281280ovmpt4g 7580 . . . . . . . . . . . 12 ((𝑗𝑌𝑖𝑋 ∧ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
282246, 61, 279, 281syl3anc 1373 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
283278, 282eqtr2d 2778 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) = (𝑗(𝐻f (.r𝐸)𝐷)𝑖))
284283mpteq2dva 5242 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))
285284oveq2d 7447 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
286267, 270, 2853eqtr3d 2785 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝐿𝑗)( ·𝑠𝐵)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
287286mpteq2dva 5242 . . . . . 6 (𝜑 → (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))))
288287oveq2d 7447 . . . . 5 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
289 ringcmn 20279 . . . . . . 7 (𝐸 ∈ Ring → 𝐸 ∈ CMnd)
29069, 289syl 17 . . . . . 6 (𝜑𝐸 ∈ CMnd)
29169adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝐸 ∈ Ring)
29238, 180eqsstrd 4018 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
293292adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
294 simprl 771 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘(Scalar‘𝐴)))
295293, 294sseldd 3984 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘𝐸))
296 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐴))
29712, 22srabase 21177 . . . . . . . . . 10 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
298297adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘𝐸) = (Base‘𝐴))
299296, 298eleqtrrd 2844 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐸))
30020, 219ringcl 20247 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
301291, 295, 299, 300syl3anc 1373 . . . . . . 7 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
30220, 219ringcl 20247 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
303232, 238, 247, 302syl3anc 1373 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
304297ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
305303, 304eleqtrd 2843 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
306305anasss 466 . . . . . . . . 9 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
307306ralrimivva 3202 . . . . . . . 8 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
308274fmpo 8093 . . . . . . . 8 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
309307, 308sylib 218 . . . . . . 7 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310 inidm 4227 . . . . . . 7 ((𝑌 × 𝑋) ∩ (𝑌 × 𝑋)) = (𝑌 × 𝑋)
311301, 65, 309, 48, 48, 310off 7715 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐸))
31269adantr 480 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝐸 ∈ Ring)
313 simpr 484 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐴))
314297adantr 480 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → (Base‘𝐸) = (Base‘𝐴))
315313, 314eleqtrrd 2844 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐸))
31620, 219, 71ringlz 20290 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑢 ∈ (Base‘𝐸)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
317312, 315, 316syl2anc 584 . . . . . . 7 ((𝜑𝑢 ∈ (Base‘𝐴)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
31848, 73, 73, 65, 309, 194, 317offinsupp1 32738 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) finSupp (0g𝐸))
31920, 71, 290, 46, 47, 311, 318gsumxp 19994 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
32012, 22sravsca 21185 . . . . . . . 8 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
321320ofeqd 7699 . . . . . . 7 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
322321oveqd 7448 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝐻f ( ·𝑠𝐴)𝐷))
323322oveq2d 7447 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
324288, 319, 3233eqtr2rd 2784 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
325 ovexd 7466 . . . . 5 (𝜑 → (𝐻f ( ·𝑠𝐴)𝐷) ∈ V)
326 fedgmullem1.a . . . . . 6 (𝜑𝑍 ∈ (Base‘𝐴))
327326elfvexd 6945 . . . . 5 (𝜑𝐴 ∈ V)
32811, 325, 67, 327, 22gsumsra 33050 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
329324, 328eqtr3d 2779 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
330198, 199, 3293eqtr2d 2783 . 2 (𝜑𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
331197, 330jca 511 1 (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  Vcvv 3480  cdif 3948  wss 3951  {csn 4626   ciun 4991   class class class wbr 5143  cmpt 5225   × cxp 5683  Fun wfun 6555  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  f cof 7695   supp csupp 8185  m cmap 8866  Fincfn 8985   finSupp cfsupp 9401  Basecbs 17247  s cress 17274  .rcmulr 17298  Scalarcsca 17300   ·𝑠 cvsca 17301  0gc0g 17484   Σg cgsu 17485  SubMndcsubmnd 18795  Grpcgrp 18951  SubGrpcsubg 19138  CMndccmn 19798  Ringcrg 20230  SubRingcsubrg 20569  DivRingcdr 20729  LModclmod 20858  LSpanclspn 20969  LBasisclbs 21073  LVecclvec 21101  subringAlg csra 21170  LIndSclinds 21825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-hom 17321  df-cco 17322  df-0g 17486  df-gsum 17487  df-prds 17492  df-pws 17494  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-mulg 19086  df-subg 19141  df-ghm 19231  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-nzr 20513  df-subrg 20570  df-drng 20731  df-lmod 20860  df-lss 20930  df-lsp 20970  df-lmhm 21021  df-lbs 21074  df-lvec 21102  df-sra 21172  df-rgmod 21173  df-dsmm 21752  df-frlm 21767  df-uvc 21803  df-lindf 21826  df-linds 21827
This theorem is referenced by:  fedgmul  33682
  Copyright terms: Public domain W3C validator