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 32201
Description: Lemma for fedgmul 32203. (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 7032 . . . . . . . . . . . 12 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5 elmapi 8783 . . . . . . . . . . . 12 ((𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
64, 5syl 17 . . . . . . . . . . 11 ((((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
76anasss 467 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
8 simprr 771 . . . . . . . . . 10 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → 𝑖𝑋)
97, 8ffvelcdmd 7032 . . . . . . . . 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 20233 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈)))
1716biimpa 477 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1813, 14, 17syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈))
1918simpld 495 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (SubRing‘𝐸))
20 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘𝐸) = (Base‘𝐸)
2120subrgss 20208 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
2219, 21syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐸))
2312, 22srasca 20631 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑉) = (Scalar‘𝐴))
2410, 23eqtrid 2788 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐴))
2518simprd 496 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑈)
26 ressabs 17122 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉𝑈) → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2713, 25, 26syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸s 𝑈) ↾s 𝑉) = (𝐸s 𝑉))
2815oveq1i 7363 . . . . . . . . . . . . . 14 (𝐹s 𝑉) = ((𝐸s 𝑈) ↾s 𝑉)
2927, 28, 103eqtr4g 2801 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = 𝐾)
30 fedgmul.c . . . . . . . . . . . . . . 15 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
3130a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = ((subringAlg ‘𝐹)‘𝑉))
32 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘𝐹) = (Base‘𝐹)
3332subrgss 20208 . . . . . . . . . . . . . . 15 (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
3414, 33syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ⊆ (Base‘𝐹))
3531, 34srasca 20631 . . . . . . . . . . . . 13 (𝜑 → (𝐹s 𝑉) = (Scalar‘𝐶))
3629, 35eqtr3d 2778 . . . . . . . . . . . 12 (𝜑𝐾 = (Scalar‘𝐶))
3724, 36eqtr3d 2778 . . . . . . . . . . 11 (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
3837fveq2d 6843 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
3938ad2antrr 724 . . . . . . . . 9 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
409, 39eleqtrrd 2841 . . . . . . . 8 (((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
4140ralrimivva 3195 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
42 fedgmullem.h . . . . . . . 8 𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
4342fmpo 7996 . . . . . . 7 (∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
4441, 43sylib 217 . . . . . 6 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45 fvexd 6854 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (Base‘(Scalar‘𝐴)) ∈ V)
46 fedgmullem.y . . . . . . . . 9 (𝜑𝑌 ∈ (LBasis‘𝐵))
47 fedgmullem.x . . . . . . . . 9 (𝜑𝑋 ∈ (LBasis‘𝐶))
4846, 47xpexd 7681 . . . . . . . 8 (𝜑 → (𝑌 × 𝑋) ∈ V)
4948adantr 481 . . . . . . 7 ((𝜑𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝑌 × 𝑋) ∈ V)
5045, 49elmapd 8775 . . . . . 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 483 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝜑)
5453adantr 481 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝜑)
551ffvelcdmda 7031 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5655, 5syl 17 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5756adantr 481 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
5838feq3d 6652 . . . . . . . . . . 11 (𝜑 → ((𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)) ↔ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))))
5958biimpar 478 . . . . . . . . . 10 ((𝜑 ∧ (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐶))) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
6054, 57, 59syl2anc 584 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝐺𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
61 simpr 485 . . . . . . . . 9 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖𝑋)
6260, 61ffvelcdmd 7032 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6362ralrimiva 3141 . . . . . . 7 ((𝜑𝑗𝑌) → ∀𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6463ralrimiva 3141 . . . . . 6 (𝜑 → ∀𝑗𝑌𝑖𝑋 ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
6564, 43sylib 217 . . . . 5 (𝜑𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
6665ffund 6669 . . . 4 (𝜑 → Fun 𝐻)
67 fedgmul.1 . . . . . 6 (𝜑𝐸 ∈ DivRing)
68 drngring 20177 . . . . . 6 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
6967, 68syl 17 . . . . 5 (𝜑𝐸 ∈ Ring)
70 ringgrp 19955 . . . . 5 (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71 eqid 2736 . . . . . 6 (0g𝐸) = (0g𝐸)
7220, 71grpidcl 18770 . . . . 5 (𝐸 ∈ Grp → (0g𝐸) ∈ (Base‘𝐸))
7369, 70, 723syl 18 . . . 4 (𝜑 → (0g𝐸) ∈ (Base‘𝐸))
74 fedgmullem1.1 . . . . . . 7 (𝜑𝐿 finSupp (0g‘(Scalar‘𝐵)))
7574fsuppimpd 9308 . . . . . 6 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ∈ Fin)
76 simpl 483 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝜑)
77 simpr 485 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵)))))
7877eldifad 3920 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗𝑌)
79 fedgmullem1.l . . . . . . . . . 10 (𝜑𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
80 ssidd 3965 . . . . . . . . . 10 (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
81 fvexd 6854 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
8279, 80, 46, 81suppssr 8123 . . . . . . . . 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 20208 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 ⊆ (Base‘𝐸))
8986, 88srasca 20631 . . . . . . . . . . . . 13 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
9015, 89eqtrid 2788 . . . . . . . . . . . 12 (𝜑𝐹 = (Scalar‘𝐵))
9190fveq2d 6843 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g‘(Scalar‘𝐵)))
92 fedgmul.2 . . . . . . . . . . . 12 (𝜑𝐹 ∈ DivRing)
9330, 92, 14drgext0g 32168 . . . . . . . . . . 11 (𝜑 → (0g𝐹) = (0g𝐶))
9491, 93eqtr3d 2778 . . . . . . . . . 10 (𝜑 → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9594adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (0g‘(Scalar‘𝐵)) = (0g𝐶))
9682, 84, 953eqtr3d 2784 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))
97 fedgmullem1.2 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)))
98 breq1 5106 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → (𝑔 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))))
99 fveq1 6838 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝐺𝑗) → (𝑔𝑖) = ((𝐺𝑗)‘𝑖))
10099oveq1d 7368 . . . . . . . . . . . . . . . 16 (𝑔 = (𝐺𝑗) → ((𝑔𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))
101100mpteq2dv 5205 . . . . . . . . . . . . . . 15 (𝑔 = (𝐺𝑗) → (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))
102101oveq2d 7369 . . . . . . . . . . . . . 14 (𝑔 = (𝐺𝑗) → (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
103102eqeq1d 2738 . . . . . . . . . . . . 13 (𝑔 = (𝐺𝑗) → ((𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) ↔ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)))
10498, 103anbi12d 631 . . . . . . . . . . . 12 (𝑔 = (𝐺𝑗) → ((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) ↔ ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶))))
105 eqeq1 2740 . . . . . . . . . . . 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 2838 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹s 𝑉) ∈ DivRing)
109 eqid 2736 . . . . . . . . . . . . . . . 16 (𝐹s 𝑉) = (𝐹s 𝑉)
11030, 109sralvec 32166 . . . . . . . . . . . . . . 15 ((𝐹 ∈ DivRing ∧ (𝐹s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
11192, 108, 14, 110syl3anc 1371 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ LVec)
112 lveclmod 20552 . . . . . . . . . . . . . 14 (𝐶 ∈ LVec → 𝐶 ∈ LMod)
113111, 112syl 17 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ LMod)
114113adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝐶 ∈ LMod)
115 eqid 2736 . . . . . . . . . . . . . . 15 (Base‘𝐶) = (Base‘𝐶)
116 eqid 2736 . . . . . . . . . . . . . . 15 (LBasis‘𝐶) = (LBasis‘𝐶)
117115, 116lbsss 20523 . . . . . . . . . . . . . 14 (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
11847, 117syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (Base‘𝐶))
119118adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ⊆ (Base‘𝐶))
120 eqid 2736 . . . . . . . . . . . . . . . 16 (LSpan‘𝐶) = (LSpan‘𝐶)
121115, 116, 120islbs4 21223 . . . . . . . . . . . . . . 15 (𝑋 ∈ (LBasis‘𝐶) ↔ (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
12247, 121sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
123122simpld 495 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ (LIndS‘𝐶))
124123adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LIndS‘𝐶))
125 eqid 2736 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
126 eqid 2736 . . . . . . . . . . . . . 14 (Scalar‘𝐶) = (Scalar‘𝐶)
127 eqid 2736 . . . . . . . . . . . . . 14 ( ·𝑠𝐶) = ( ·𝑠𝐶)
128 eqid 2736 . . . . . . . . . . . . . 14 (0g𝐶) = (0g𝐶)
129 eqid 2736 . . . . . . . . . . . . . 14 (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
130115, 125, 126, 127, 128, 129islinds5 32039 . . . . . . . . . . . . 13 ((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) → (𝑋 ∈ (LIndS‘𝐶) ↔ ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ ((𝑔𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
131130biimpa 477 . . . . . . . . . . . 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 3580 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
13497, 133mpand 693 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
135134imp 407 . . . . . . . 8 (((𝜑𝑗𝑌) ∧ (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (0g𝐶)) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
13676, 78, 96, 135syl21anc 836 . . . . . . 7 ((𝜑𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐺𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
1371, 136suppss 8121 . . . . . 6 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
13875, 137ssfid 9207 . . . . 5 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139 suppssdm 8104 . . . . . . . . . 10 (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140139, 1fssdm 6685 . . . . . . . . 9 (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141140sselda 3942 . . . . . . . 8 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤𝑌)
142 eleq1w 2820 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝑗𝑌𝑤𝑌))
143142anbi2d 629 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝜑𝑗𝑌) ↔ (𝜑𝑤𝑌)))
144 fveq2 6839 . . . . . . . . . . . 12 (𝑗 = 𝑤 → (𝐺𝑗) = (𝐺𝑤))
145144breq1d 5113 . . . . . . . . . . 11 (𝑗 = 𝑤 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶))))
146143, 145imbi12d 344 . . . . . . . . . 10 (𝑗 = 𝑤 → (((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g‘(Scalar‘𝐶))) ↔ ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))))
147146, 97chvarvv 2002 . . . . . . . . 9 ((𝜑𝑤𝑌) → (𝐺𝑤) finSupp (0g‘(Scalar‘𝐶)))
148147fsuppimpd 9308 . . . . . . . 8 ((𝜑𝑤𝑌) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
149141, 148syldan 591 . . . . . . 7 ((𝜑𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
150149ralrimiva 3141 . . . . . 6 (𝜑 → ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
151 iunfi 9280 . . . . . 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 9257 . . . . 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 6839 . . . . . . . . . 10 (𝑣 = 𝑗 → (𝐺𝑣) = (𝐺𝑗))
156155fveq1d 6841 . . . . . . . . 9 (𝑣 = 𝑗 → ((𝐺𝑣)‘𝑢) = ((𝐺𝑗)‘𝑢))
157156mpteq2dv 5205 . . . . . . . 8 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)))
158 fveq2 6839 . . . . . . . . 9 (𝑢 = 𝑖 → ((𝐺𝑗)‘𝑢) = ((𝐺𝑗)‘𝑖))
159158cbvmptv 5216 . . . . . . . 8 (𝑢𝑋 ↦ ((𝐺𝑗)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖))
160157, 159eqtrdi 2792 . . . . . . 7 (𝑣 = 𝑗 → (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)) = (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
161160cbvmptv 5216 . . . . . 6 (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = (𝑗𝑌 ↦ (𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
162 fvexd 6854 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163 fvexd 6854 . . . . . 6 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → ((𝐺𝑗)‘𝑖) ∈ V)
16442, 161, 46, 47, 162, 163suppovss 31482 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
16510, 71subrg0 20214 . . . . . . . 8 (𝑉 ∈ (SubRing‘𝐸) → (0g𝐸) = (0g𝐾))
16619, 165syl 17 . . . . . . 7 (𝜑 → (0g𝐸) = (0g𝐾))
16736fveq2d 6843 . . . . . . 7 (𝜑 → (0g𝐾) = (0g‘(Scalar‘𝐶)))
168166, 167eqtr2d 2777 . . . . . 6 (𝜑 → (0g‘(Scalar‘𝐶)) = (0g𝐸))
169168oveq2d 7369 . . . . 5 (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g𝐸)))
1701feqmptd 6907 . . . . . . . 8 (𝜑𝐺 = (𝑣𝑌 ↦ (𝐺𝑣)))
171 eleq1w 2820 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝑗𝑌𝑣𝑌))
172171anbi2d 629 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝜑𝑗𝑌) ↔ (𝜑𝑣𝑌)))
173 fveq2 6839 . . . . . . . . . . . . 13 (𝑗 = 𝑣 → (𝐺𝑗) = (𝐺𝑣))
174173feq1d 6650 . . . . . . . . . . . 12 (𝑗 = 𝑣 → ((𝐺𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺𝑣):𝑋⟶(Base‘𝐸)))
175172, 174imbi12d 344 . . . . . . . . . . 11 (𝑗 = 𝑣 → (((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))))
17610, 20ressbas2 17112 . . . . . . . . . . . . . . . 16 (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
17722, 176syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉 = (Base‘𝐾))
17836fveq2d 6843 . . . . . . . . . . . . . . 15 (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
179177, 178eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑𝑉 = (Base‘(Scalar‘𝐶)))
180179, 22eqsstrrd 3981 . . . . . . . . . . . . 13 (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
181180adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
18256, 181fssd 6683 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐺𝑗):𝑋⟶(Base‘𝐸))
183175, 182chvarvv 2002 . . . . . . . . . 10 ((𝜑𝑣𝑌) → (𝐺𝑣):𝑋⟶(Base‘𝐸))
184183feqmptd 6907 . . . . . . . . 9 ((𝜑𝑣𝑌) → (𝐺𝑣) = (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))
185184mpteq2dva 5203 . . . . . . . 8 (𝜑 → (𝑣𝑌 ↦ (𝐺𝑣)) = (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))))
186170, 185eqtr2d 2777 . . . . . . 7 (𝜑 → (𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) = 𝐺)
187186oveq1d 7368 . . . . . 6 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188186fveq1d 6841 . . . . . . . 8 (𝜑 → ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) = (𝐺𝑤))
189188oveq1d 7368 . . . . . . 7 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
190187, 189iuneq12d 4980 . . . . . 6 (𝜑 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶))))
191187, 190xpeq12d 5662 . . . . 5 (𝜑 → (((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ ((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣𝑌 ↦ (𝑢𝑋 ↦ ((𝐺𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))) = ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
192164, 169, 1913sstr3d 3988 . . . 4 (𝜑 → (𝐻 supp (0g𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺𝑤) supp (0g‘(Scalar‘𝐶)))))
193 suppssfifsupp 9316 . . . 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 1378 . . 3 (𝜑𝐻 finSupp (0g𝐸))
19537fveq2d 6843 . . . 4 (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
196195, 168eqtr2d 2777 . . 3 (𝜑 → (0g𝐸) = (0g‘(Scalar‘𝐴)))
197194, 196breqtrd 5129 . 2 (𝜑𝐻 finSupp (0g‘(Scalar‘𝐴)))
198 fedgmullem1.z . . 3 (𝜑𝑍 = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
19985, 67, 13, 15, 92, 46drgextgsum 32173 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐵 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
20047adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑋 ∈ (LBasis‘𝐶))
20113adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202 subrgsubg 20213 . . . . . . . . . . . . 13 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203 subgsubm 18941 . . . . . . . . . . . . 13 (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204201, 202, 2033syl 18 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205113ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐶 ∈ LMod)
20656ffvelcdmda 7031 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207118ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐶))
208207, 61sseldd 3943 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐶))
209115, 126, 127, 125lmodvscl 20324 . . . . . . . . . . . . . . 15 ((𝐶 ∈ LMod ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
210205, 206, 208, 209syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ (Base‘𝐶))
21115, 20ressbas2 17112 . . . . . . . . . . . . . . . . 17 (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
21288, 211syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑈 = (Base‘𝐹))
21331, 34srabase 20625 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐹) = (Base‘𝐶))
214212, 213eqtrd 2776 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝐶))
215214ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑈 = (Base‘𝐶))
216210, 215eleqtrrd 2841 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) ∈ 𝑈)
217216fmpttd 7059 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)):𝑋𝑈)
218200, 204, 217, 15gsumsubm 18637 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
219 eqid 2736 . . . . . . . . . . . . . . . . . 18 (.r𝐸) = (.r𝐸)
22015, 219ressmulr 17180 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ (SubRing‘𝐸) → (.r𝐸) = (.r𝐹))
22113, 220syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐸) = (.r𝐹))
22231, 34sravsca 20633 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝐹) = ( ·𝑠𝐶))
223221, 222eqtr2d 2777 . . . . . . . . . . . . . . 15 (𝜑 → ( ·𝑠𝐶) = (.r𝐸))
224223ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ( ·𝑠𝐶) = (.r𝐸))
225224oveqd 7370 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))
226225mpteq2dva 5203 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))
227226oveq2d 7369 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))))
22830, 92, 14, 109, 108, 47drgextgsum 32173 . . . . . . . . . . . 12 (𝜑 → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
229228adantr 481 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝐹 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
230218, 227, 2293eqtr3d 2784 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖))) = (𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖))))
231230oveq1d 7368 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
23269ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝐸 ∈ Ring)
233180ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
234233, 206sseldd 3943 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸))
235214, 88eqsstrrd 3981 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
236118, 235sstrd 3952 . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ (Base‘𝐸))
237236ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑋 ⊆ (Base‘𝐸))
238237, 61sseldd 3943 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑖 ∈ (Base‘𝐸))
239 eqid 2736 . . . . . . . . . . . . . . . . . 18 (Base‘𝐵) = (Base‘𝐵)
240 eqid 2736 . . . . . . . . . . . . . . . . . 18 (LBasis‘𝐵) = (LBasis‘𝐵)
241239, 240lbsss 20523 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
24246, 241syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ⊆ (Base‘𝐵))
24386, 88srabase 20625 . . . . . . . . . . . . . . . 16 (𝜑 → (Base‘𝐸) = (Base‘𝐵))
244242, 243sseqtrrd 3983 . . . . . . . . . . . . . . 15 (𝜑𝑌 ⊆ (Base‘𝐸))
245244ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑌 ⊆ (Base‘𝐸))
246 simplr 767 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗𝑌)
247245, 246sseldd 3943 . . . . . . . . . . . . 13 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → 𝑗 ∈ (Base‘𝐸))
24820, 219ringass 19970 . . . . . . . . . . . . 13 ((𝐸 ∈ Ring ∧ (((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
249232, 234, 238, 247, 248syl13anc 1372 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
250249mpteq2dva 5203 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗)) = (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
251250oveq2d 7369 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
252 eqid 2736 . . . . . . . . . . 11 (+g𝐸) = (+g𝐸)
25369adantr 481 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝐸 ∈ Ring)
254242adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐵))
255243adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → (Base‘𝐸) = (Base‘𝐵))
256254, 255sseqtrrd 3983 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑌 ⊆ (Base‘𝐸))
257 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → 𝑗𝑌)
258256, 257sseldd 3943 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → 𝑗 ∈ (Base‘𝐸))
25920, 219ringcl 19967 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ ((𝐺𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
260232, 234, 238, 259syl3anc 1371 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖) ∈ (Base‘𝐸))
261168breq2d 5115 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
262261adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗𝑌) → ((𝐺𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺𝑗) finSupp (0g𝐸)))
26397, 262mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑗𝑌) → (𝐺𝑗) finSupp (0g𝐸))
26420, 253, 200, 238, 182, 263rmfsupp2 31958 . . . . . . . . . . 11 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)) finSupp (0g𝐸))
26520, 71, 252, 219, 253, 200, 258, 260, 264gsummulc1 20015 . . . . . . . . . 10 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ ((((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)(.r𝐸)𝑗))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
266251, 265eqtr3d 2778 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = ((𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)𝑖)))(.r𝐸)𝑗))
26783oveq1d 7368 . . . . . . . . 9 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐶 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)( ·𝑠𝐶)𝑖)))(.r𝐸)𝑗))
268231, 266, 2673eqtr4rd 2787 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))))
26986, 88sravsca 20633 . . . . . . . . . 10 (𝜑 → (.r𝐸) = ( ·𝑠𝐵))
270269adantr 481 . . . . . . . . 9 ((𝜑𝑗𝑌) → (.r𝐸) = ( ·𝑠𝐵))
271270oveqd 7370 . . . . . . . 8 ((𝜑𝑗𝑌) → ((𝐿𝑗)(.r𝐸)𝑗) = ((𝐿𝑗)( ·𝑠𝐵)𝑗))
272 fvexd 6854 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → ((𝐺𝑗)‘𝑖) ∈ V)
273 ovexd 7388 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑌𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ V)
27442a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝑗𝑌, 𝑖𝑋 ↦ ((𝐺𝑗)‘𝑖)))
275 fedgmullem.d . . . . . . . . . . . . . . 15 𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗))
276275a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐷 = (𝑗𝑌, 𝑖𝑋 ↦ (𝑖(.r𝐸)𝑗)))
27746, 47, 272, 273, 274, 276offval22 8016 . . . . . . . . . . . . 13 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))))
278277oveqd 7370 . . . . . . . . . . . 12 (𝜑 → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
279278ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝐻f (.r𝐸)𝐷)𝑖) = (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖))
280 ovexd 7388 . . . . . . . . . . . 12 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V)
281 eqid 2736 . . . . . . . . . . . . 13 (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
282281ovmpt4g 7498 . . . . . . . . . . . 12 ((𝑗𝑌𝑖𝑋 ∧ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) ∈ V) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
283246, 61, 280, 282syl3anc 1371 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑗(𝑗𝑌, 𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))𝑖) = (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))
284279, 283eqtr2d 2777 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)) = (𝑗(𝐻f (.r𝐸)𝐷)𝑖))
285284mpteq2dva 5203 . . . . . . . . 9 ((𝜑𝑗𝑌) → (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗))) = (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))
286285oveq2d 7369 . . . . . . . 8 ((𝜑𝑗𝑌) → (𝐸 Σg (𝑖𝑋 ↦ (((𝐺𝑗)‘𝑖)(.r𝐸)(𝑖(.r𝐸)𝑗)))) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
287268, 271, 2863eqtr3d 2784 . . . . . . 7 ((𝜑𝑗𝑌) → ((𝐿𝑗)( ·𝑠𝐵)𝑗) = (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))
288287mpteq2dva 5203 . . . . . 6 (𝜑 → (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗)) = (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖)))))
289288oveq2d 7369 . . . . 5 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
290 ringcmn 19988 . . . . . . 7 (𝐸 ∈ Ring → 𝐸 ∈ CMnd)
29169, 290syl 17 . . . . . 6 (𝜑𝐸 ∈ CMnd)
29269adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝐸 ∈ Ring)
29338, 180eqsstrd 3980 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
294293adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
295 simprl 769 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘(Scalar‘𝐴)))
296294, 295sseldd 3943 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘𝐸))
297 simprr 771 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐴))
29812, 22srabase 20625 . . . . . . . . . 10 (𝜑 → (Base‘𝐸) = (Base‘𝐴))
299298adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘𝐸) = (Base‘𝐴))
300297, 299eleqtrrd 2841 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐸))
30120, 219ringcl 19967 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
302292, 296, 300, 301syl3anc 1371 . . . . . . 7 ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r𝐸)𝑘) ∈ (Base‘𝐸))
30320, 219ringcl 19967 . . . . . . . . . . . 12 ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
304232, 238, 247, 303syl3anc 1371 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐸))
305298ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (Base‘𝐸) = (Base‘𝐴))
306304, 305eleqtrd 2840 . . . . . . . . . 10 (((𝜑𝑗𝑌) ∧ 𝑖𝑋) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
307306anasss 467 . . . . . . . . 9 ((𝜑 ∧ (𝑗𝑌𝑖𝑋)) → (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
308307ralrimivva 3195 . . . . . . . 8 (𝜑 → ∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴))
309275fmpo 7996 . . . . . . . 8 (∀𝑗𝑌𝑖𝑋 (𝑖(.r𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310308, 309sylib 217 . . . . . . 7 (𝜑𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
311 inidm 4176 . . . . . . 7 ((𝑌 × 𝑋) ∩ (𝑌 × 𝑋)) = (𝑌 × 𝑋)
312302, 65, 310, 48, 48, 311off 7631 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐸))
31369adantr 481 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝐸 ∈ Ring)
314 simpr 485 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐴))
315298adantr 481 . . . . . . . . 9 ((𝜑𝑢 ∈ (Base‘𝐴)) → (Base‘𝐸) = (Base‘𝐴))
316314, 315eleqtrrd 2841 . . . . . . . 8 ((𝜑𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐸))
31720, 219, 71ringlz 19996 . . . . . . . 8 ((𝐸 ∈ Ring ∧ 𝑢 ∈ (Base‘𝐸)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
318313, 316, 317syl2anc 584 . . . . . . 7 ((𝜑𝑢 ∈ (Base‘𝐴)) → ((0g𝐸)(.r𝐸)𝑢) = (0g𝐸))
31948, 73, 73, 65, 310, 194, 318offinsupp1 31527 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) finSupp (0g𝐸))
32020, 71, 291, 46, 47, 312, 319gsumxp 19744 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ (𝐸 Σg (𝑖𝑋 ↦ (𝑗(𝐻f (.r𝐸)𝐷)𝑖))))))
32112, 22sravsca 20633 . . . . . . . 8 (𝜑 → (.r𝐸) = ( ·𝑠𝐴))
322321ofeqd 7615 . . . . . . 7 (𝜑 → ∘f (.r𝐸) = ∘f ( ·𝑠𝐴))
323322oveqd 7370 . . . . . 6 (𝜑 → (𝐻f (.r𝐸)𝐷) = (𝐻f ( ·𝑠𝐴)𝐷))
324323oveq2d 7369 . . . . 5 (𝜑 → (𝐸 Σg (𝐻f (.r𝐸)𝐷)) = (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
325289, 320, 3243eqtr2rd 2783 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))))
326 ovexd 7388 . . . . 5 (𝜑 → (𝐻f ( ·𝑠𝐴)𝐷) ∈ V)
327 fedgmullem1.a . . . . . 6 (𝜑𝑍 ∈ (Base‘𝐴))
328327elfvexd 6878 . . . . 5 (𝜑𝐴 ∈ V)
32911, 326, 67, 328, 22gsumsra 31772 . . . 4 (𝜑 → (𝐸 Σg (𝐻f ( ·𝑠𝐴)𝐷)) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
330325, 329eqtr3d 2778 . . 3 (𝜑 → (𝐸 Σg (𝑗𝑌 ↦ ((𝐿𝑗)( ·𝑠𝐵)𝑗))) = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
331198, 199, 3303eqtr2d 2782 . 2 (𝜑𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷)))
332197, 331jca 512 1 (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻f ( ·𝑠𝐴)𝐷))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3062  Vcvv 3443  cdif 3905  wss 3908  {csn 4584   ciun 4952   class class class wbr 5103  cmpt 5186   × cxp 5629  Fun wfun 6487  wf 6489  cfv 6493  (class class class)co 7353  cmpo 7355  f cof 7611   supp csupp 8088  m cmap 8761  Fincfn 8879   finSupp cfsupp 9301  Basecbs 17075  s cress 17104  +gcplusg 17125  .rcmulr 17126  Scalarcsca 17128   ·𝑠 cvsca 17129  0gc0g 17313   Σg cgsu 17314  SubMndcsubmnd 18592  Grpcgrp 18740  SubGrpcsubg 18913  CMndccmn 19553  Ringcrg 19950  DivRingcdr 20170  SubRingcsubrg 20203  LModclmod 20307  LSpanclspn 20417  LBasisclbs 20520  LVecclvec 20548  subringAlg csra 20614  LIndSclinds 21196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-cnex 11103  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123  ax-pre-mulgt0 11124
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7309  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7613  df-om 7799  df-1st 7917  df-2nd 7918  df-supp 8089  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-1o 8408  df-er 8644  df-map 8763  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9302  df-sup 9374  df-oi 9442  df-card 9871  df-pnf 11187  df-mnf 11188  df-xr 11189  df-ltxr 11190  df-le 11191  df-sub 11383  df-neg 11384  df-nn 12150  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-6 12216  df-7 12217  df-8 12218  df-9 12219  df-n0 12410  df-z 12496  df-dec 12615  df-uz 12760  df-fz 13417  df-fzo 13560  df-seq 13899  df-hash 14223  df-struct 17011  df-sets 17028  df-slot 17046  df-ndx 17058  df-base 17076  df-ress 17105  df-plusg 17138  df-mulr 17139  df-sca 17141  df-vsca 17142  df-ip 17143  df-tset 17144  df-ple 17145  df-ds 17147  df-hom 17149  df-cco 17150  df-0g 17315  df-gsum 17316  df-prds 17321  df-pws 17323  df-mre 17458  df-mrc 17459  df-acs 17461  df-mgm 18489  df-sgrp 18538  df-mnd 18549  df-mhm 18593  df-submnd 18594  df-grp 18743  df-minusg 18744  df-sbg 18745  df-mulg 18864  df-subg 18916  df-ghm 18997  df-cntz 19088  df-cmn 19555  df-abl 19556  df-mgp 19888  df-ur 19905  df-ring 19952  df-drng 20172  df-subrg 20205  df-lmod 20309  df-lss 20378  df-lsp 20418  df-lmhm 20468  df-lbs 20521  df-lvec 20549  df-sra 20618  df-rgmod 20619  df-nzr 20713  df-dsmm 21123  df-frlm 21138  df-uvc 21174  df-lindf 21197  df-linds 21198
This theorem is referenced by:  fedgmul  32203
  Copyright terms: Public domain W3C validator