This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fedgmullem1

Description: Lemma for fedgmul . (Contributed by Thierry Arnoux, 20-Jul-2023)

Ref Expression
Hypotheses 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 fedgmullem1 ( 𝜑 → ( 𝐻 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑍 = ( 𝐴 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 fedgmul.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑉 )
2 fedgmul.b ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
3 fedgmul.c ⊢ 𝐶 = ( ( subringAlg ‘ 𝐹 ) ‘ 𝑉 )
4 fedgmul.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
5 fedgmul.k ⊢ 𝐾 = ( 𝐸 ↾s 𝑉 )
6 fedgmul.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
7 fedgmul.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
8 fedgmul.3 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
9 fedgmul.4 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
10 fedgmul.5 ⊢ ( 𝜑 → 𝑉 ∈ ( SubRing ‘ 𝐹 ) )
11 fedgmullem.d ⊢ 𝐷 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) )
12 fedgmullem.h ⊢ 𝐻 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) )
13 fedgmullem.x ⊢ ( 𝜑 → 𝑋 ∈ ( LBasis ‘ 𝐶 ) )
14 fedgmullem.y ⊢ ( 𝜑 → 𝑌 ∈ ( LBasis ‘ 𝐵 ) )
15 fedgmullem1.a ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐴 ) )
16 fedgmullem1.l ⊢ ( 𝜑 → 𝐿 : 𝑌 ⟶ ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
17 fedgmullem1.1 ⊢ ( 𝜑 → 𝐿 finSupp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
18 fedgmullem1.z ⊢ ( 𝜑 → 𝑍 = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
19 fedgmullem1.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) )
20 fedgmullem1.2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) )
21 fedgmullem1.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐿 ‘ 𝑗 ) = ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ 𝑌 )
24 22 23 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) )
25 elmapi ⊢ ( ( 𝐺 ‘ 𝑗 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
26 24 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
27 26 anasss ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
28 simprr ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → 𝑖 ∈ 𝑋 )
29 27 28 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
30 1 a1i ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑉 ) )
31 4 subsubrg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( 𝑉 ∈ ( SubRing ‘ 𝐹 ) ↔ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) ) )
32 31 biimpa ⊢ ( ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ∈ ( SubRing ‘ 𝐹 ) ) → ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) )
33 9 10 32 syl2anc ⊢ ( 𝜑 → ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) )
34 33 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( SubRing ‘ 𝐸 ) )
35 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
36 35 subrgss ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
37 34 36 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝐸 ) )
38 30 37 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝑉 ) = ( Scalar ‘ 𝐴 ) )
39 5 38 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝐴 ) )
40 33 simprd ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
41 ressabs ⊢ ( ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝐸 ↾s 𝑈 ) ↾s 𝑉 ) = ( 𝐸 ↾s 𝑉 ) )
42 9 40 41 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ↾s 𝑈 ) ↾s 𝑉 ) = ( 𝐸 ↾s 𝑉 ) )
43 4 oveq1i ⊢ ( 𝐹 ↾s 𝑉 ) = ( ( 𝐸 ↾s 𝑈 ) ↾s 𝑉 )
44 42 43 5 3eqtr4g ⊢ ( 𝜑 → ( 𝐹 ↾s 𝑉 ) = 𝐾 )
45 3 a1i ⊢ ( 𝜑 → 𝐶 = ( ( subringAlg ‘ 𝐹 ) ‘ 𝑉 ) )
46 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
47 46 subrgss ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐹 ) → 𝑉 ⊆ ( Base ‘ 𝐹 ) )
48 10 47 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝐹 ) )
49 45 48 srasca ⊢ ( 𝜑 → ( 𝐹 ↾s 𝑉 ) = ( Scalar ‘ 𝐶 ) )
50 44 49 eqtr3d ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝐶 ) )
51 39 50 eqtr3d ⊢ ( 𝜑 → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐶 ) )
52 51 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
54 29 53 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
55 54 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
56 12 fmpo ⊢ ( ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↔ 𝐻 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
57 55 56 sylib ⊢ ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) → 𝐻 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
58 fvexd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∈ V )
59 14 13 xpexd ⊢ ( 𝜑 → ( 𝑌 × 𝑋 ) ∈ V )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) → ( 𝑌 × 𝑋 ) ∈ V )
61 58 60 elmapd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) → ( 𝐻 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) ↔ 𝐻 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
62 57 61 mpbird ⊢ ( ( 𝜑 ∧ 𝐺 : 𝑌 ⟶ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ) → 𝐻 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) )
63 19 62 mpdan ⊢ ( 𝜑 → 𝐻 ∈ ( ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↑m ( 𝑌 × 𝑋 ) ) )
64 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝜑 )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝜑 )
66 19 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) )
67 66 25 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
69 52 feq3d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) )
70 69 biimpar ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
71 65 68 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
72 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
73 71 72 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
74 73 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ∀ 𝑖 ∈ 𝑋 ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
75 74 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
76 75 56 sylib ⊢ ( 𝜑 → 𝐻 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
77 76 ffund ⊢ ( 𝜑 → Fun 𝐻 )
78 drngring ⊢ ( 𝐸 ∈ DivRing → 𝐸 ∈ Ring )
79 6 78 syl ⊢ ( 𝜑 → 𝐸 ∈ Ring )
80 ringgrp ⊢ ( 𝐸 ∈ Ring → 𝐸 ∈ Grp )
81 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
82 35 81 grpidcl ⊢ ( 𝐸 ∈ Grp → ( 0g ‘ 𝐸 ) ∈ ( Base ‘ 𝐸 ) )
83 79 80 82 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ ( Base ‘ 𝐸 ) )
84 17 fsuppimpd ⊢ ( 𝜑 → ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ∈ Fin )
85 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → 𝜑 )
86 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) )
87 86 eldifad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → 𝑗 ∈ 𝑌 )
88 ssidd ⊢ ( 𝜑 → ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ⊆ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
89 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ∈ V )
90 16 88 14 89 suppssr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → ( 𝐿 ‘ 𝑗 ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
91 87 21 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → ( 𝐿 ‘ 𝑗 ) = ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
92 2 a1i ⊢ ( 𝜑 → 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
93 35 subrgss ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
94 9 93 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
95 92 94 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝑈 ) = ( Scalar ‘ 𝐵 ) )
96 4 95 eqtrid ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐵 ) )
97 96 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
98 3 7 10 drgext0g ⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐶 ) )
99 97 98 eqtr3d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ 𝐶 ) )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → ( 0g ‘ ( Scalar ‘ 𝐵 ) ) = ( 0g ‘ 𝐶 ) )
101 90 91 100 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) )
102 breq1 ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( 𝑔 finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ↔ ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) )
103 fveq1 ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( 𝑔 ‘ 𝑖 ) = ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) )
104 103 oveq1d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) = ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) )
105 104 mpteq2dv ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) )
106 105 oveq2d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
107 106 eqeq1d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ↔ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) )
108 102 107 anbi12d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( ( 𝑔 finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) ↔ ( ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
109 eqeq1 ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( 𝑔 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ↔ ( 𝐺 ‘ 𝑗 ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) )
110 108 109 imbi12d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑗 ) → ( ( ( 𝑔 finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → 𝑔 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ↔ ( ( ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝑗 ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ) )
111 44 8 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ↾s 𝑉 ) ∈ DivRing )
112 eqid ⊢ ( 𝐹 ↾s 𝑉 ) = ( 𝐹 ↾s 𝑉 )
113 3 112 sralvec ⊢ ( ( 𝐹 ∈ DivRing ∧ ( 𝐹 ↾s 𝑉 ) ∈ DivRing ∧ 𝑉 ∈ ( SubRing ‘ 𝐹 ) ) → 𝐶 ∈ LVec )
114 7 111 10 113 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ LVec )
115 lveclmod ⊢ ( 𝐶 ∈ LVec → 𝐶 ∈ LMod )
116 114 115 syl ⊢ ( 𝜑 → 𝐶 ∈ LMod )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐶 ∈ LMod )
118 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
119 eqid ⊢ ( LBasis ‘ 𝐶 ) = ( LBasis ‘ 𝐶 )
120 118 119 lbsss ⊢ ( 𝑋 ∈ ( LBasis ‘ 𝐶 ) → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
121 13 120 syl ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
123 eqid ⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
124 118 119 123 islbs4 ⊢ ( 𝑋 ∈ ( LBasis ‘ 𝐶 ) ↔ ( 𝑋 ∈ ( LIndS ‘ 𝐶 ) ∧ ( ( LSpan ‘ 𝐶 ) ‘ 𝑋 ) = ( Base ‘ 𝐶 ) ) )
125 13 124 sylib ⊢ ( 𝜑 → ( 𝑋 ∈ ( LIndS ‘ 𝐶 ) ∧ ( ( LSpan ‘ 𝐶 ) ‘ 𝑋 ) = ( Base ‘ 𝐶 ) ) )
126 125 simpld ⊢ ( 𝜑 → 𝑋 ∈ ( LIndS ‘ 𝐶 ) )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑋 ∈ ( LIndS ‘ 𝐶 ) )
128 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
129 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
130 eqid ⊢ ( ·𝑠 ‘ 𝐶 ) = ( ·𝑠 ‘ 𝐶 )
131 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
132 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) )
133 118 128 129 130 131 132 islinds5 ⊢ ( ( 𝐶 ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ 𝐶 ) ) → ( 𝑋 ∈ ( LIndS ‘ 𝐶 ) ↔ ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ( ( 𝑔 finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → 𝑔 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ) )
134 133 biimpa ⊢ ( ( ( 𝐶 ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ 𝐶 ) ) ∧ 𝑋 ∈ ( LIndS ‘ 𝐶 ) ) → ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ( ( 𝑔 finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → 𝑔 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) )
135 117 122 127 134 syl21anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ↑m 𝑋 ) ( ( 𝑔 finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( 𝑔 ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → 𝑔 = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) )
136 110 135 66 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝑗 ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) )
137 20 136 mpand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) → ( 𝐺 ‘ 𝑗 ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) )
138 137 imp ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 0g ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝑗 ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) )
139 85 87 101 138 syl21anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑌 ∖ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) ) ) → ( 𝐺 ‘ 𝑗 ) = ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) )
140 19 139 suppss ⊢ ( 𝜑 → ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ⊆ ( 𝐿 supp ( 0g ‘ ( Scalar ‘ 𝐵 ) ) ) )
141 84 140 ssfid ⊢ ( 𝜑 → ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ∈ Fin )
142 suppssdm ⊢ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ⊆ dom 𝐺
143 142 19 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ⊆ 𝑌 )
144 143 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ) → 𝑤 ∈ 𝑌 )
145 eleq1w ⊢ ( 𝑗 = 𝑤 → ( 𝑗 ∈ 𝑌 ↔ 𝑤 ∈ 𝑌 ) )
146 145 anbi2d ⊢ ( 𝑗 = 𝑤 → ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ↔ ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ) )
147 fveq2 ⊢ ( 𝑗 = 𝑤 → ( 𝐺 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑤 ) )
148 147 breq1d ⊢ ( 𝑗 = 𝑤 → ( ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ↔ ( 𝐺 ‘ 𝑤 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) )
149 146 148 imbi12d ⊢ ( 𝑗 = 𝑤 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑤 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) )
150 149 20 chvarvv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑤 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) )
151 150 fsuppimpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin )
152 144 151 syldan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ) → ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin )
153 152 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin )
154 iunfi ⊢ ( ( ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ∈ Fin ∧ ∀ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin ) → ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin )
155 141 153 154 syl2anc ⊢ ( 𝜑 → ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin )
156 xpfi ⊢ ( ( ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ∈ Fin ∧ ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ∈ Fin ) → ( ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) × ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) ∈ Fin )
157 141 155 156 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) × ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) ∈ Fin )
158 fveq2 ⊢ ( 𝑣 = 𝑗 → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑗 ) )
159 158 fveq1d ⊢ ( 𝑣 = 𝑗 → ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) = ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑢 ) )
160 159 mpteq2dv ⊢ ( 𝑣 = 𝑗 → ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) = ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑢 ) ) )
161 fveq2 ⊢ ( 𝑢 = 𝑖 → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑢 ) = ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) )
162 161 cbvmptv ⊢ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑢 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) )
163 160 162 eqtrdi ⊢ ( 𝑣 = 𝑗 → ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ) )
164 163 cbvmptv ⊢ ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ) )
165 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ∈ V )
166 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ V )
167 12 164 14 13 165 166 suppovss ⊢ ( 𝜑 → ( 𝐻 supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ⊆ ( ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) × ∪ 𝑤 ∈ ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) )
168 5 81 subrg0 ⊢ ( 𝑉 ∈ ( SubRing ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐾 ) )
169 34 168 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐾 ) )
170 50 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) ) )
171 169 170 eqtr2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ 𝐸 ) )
172 171 oveq2d ⊢ ( 𝜑 → ( 𝐻 supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) = ( 𝐻 supp ( 0g ‘ 𝐸 ) ) )
173 19 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑣 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑣 ) ) )
174 eleq1w ⊢ ( 𝑗 = 𝑣 → ( 𝑗 ∈ 𝑌 ↔ 𝑣 ∈ 𝑌 ) )
175 174 anbi2d ⊢ ( 𝑗 = 𝑣 → ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ↔ ( 𝜑 ∧ 𝑣 ∈ 𝑌 ) ) )
176 fveq2 ⊢ ( 𝑗 = 𝑣 → ( 𝐺 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑣 ) )
177 176 feq1d ⊢ ( 𝑗 = 𝑣 → ( ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ 𝐸 ) ↔ ( 𝐺 ‘ 𝑣 ) : 𝑋 ⟶ ( Base ‘ 𝐸 ) ) )
178 175 177 imbi12d ⊢ ( 𝑗 = 𝑣 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ 𝐸 ) ) ↔ ( ( 𝜑 ∧ 𝑣 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑣 ) : 𝑋 ⟶ ( Base ‘ 𝐸 ) ) ) )
179 5 35 ressbas2 ⊢ ( 𝑉 ⊆ ( Base ‘ 𝐸 ) → 𝑉 = ( Base ‘ 𝐾 ) )
180 37 179 syl ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝐾 ) )
181 50 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
182 180 181 eqtrd ⊢ ( 𝜑 → 𝑉 = ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
183 182 37 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
184 183 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
185 67 184 fssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) : 𝑋 ⟶ ( Base ‘ 𝐸 ) )
186 178 185 chvarvv ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑣 ) : 𝑋 ⟶ ( Base ‘ 𝐸 ) )
187 186 feqmptd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑣 ) = ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) )
188 187 mpteq2dva ⊢ ( 𝜑 → ( 𝑣 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑣 ) ) = ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) )
189 173 188 eqtr2d ⊢ ( 𝜑 → ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) = 𝐺 )
190 189 oveq1d ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) = ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) )
191 189 fveq1d ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
192 191 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) = ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) )
193 190 192 iuneq12d ⊢ ( 𝜑 → ∪ 𝑤 ∈ ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) = ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) )
194 190 193 xpeq12d ⊢ ( 𝜑 → ( ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) × ∪ 𝑤 ∈ ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( ( 𝑣 ∈ 𝑌 ↦ ( 𝑢 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑣 ) ‘ 𝑢 ) ) ) ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) = ( ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) × ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) )
195 167 172 194 3sstr3d ⊢ ( 𝜑 → ( 𝐻 supp ( 0g ‘ 𝐸 ) ) ⊆ ( ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) × ∪ 𝑤 ∈ ( 𝐺 supp ( 𝑋 × { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ) ( ( 𝐺 ‘ 𝑤 ) supp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ) ) )
196 suppssfifsupp ⊢ ( ( ( 𝐻 ∈ ( ( 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 ‘ 𝐸 ) )
197 63 77 83 157 195 196 syl32anc ⊢ ( 𝜑 → 𝐻 finSupp ( 0g ‘ 𝐸 ) )
198 51 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) ) )
199 198 171 eqtr2d ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
200 197 199 breqtrd ⊢ ( 𝜑 → 𝐻 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
201 2 6 9 4 7 14 drgextgsum ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐵 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
202 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑋 ∈ ( LBasis ‘ 𝐶 ) )
203 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
204 subrgsubg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ∈ ( SubGrp ‘ 𝐸 ) )
205 subgsubm ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐸 ) → 𝑈 ∈ ( SubMnd ‘ 𝐸 ) )
206 203 204 205 3syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑈 ∈ ( SubMnd ‘ 𝐸 ) )
207 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐶 ∈ LMod )
208 67 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
209 121 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑋 ⊆ ( Base ‘ 𝐶 ) )
210 209 72 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐶 ) )
211 118 129 130 128 lmodvscl ⊢ ( ( 𝐶 ∈ LMod ∧ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑖 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ∈ ( Base ‘ 𝐶 ) )
212 207 208 210 211 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ∈ ( Base ‘ 𝐶 ) )
213 4 35 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝐸 ) → 𝑈 = ( Base ‘ 𝐹 ) )
214 94 213 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐹 ) )
215 45 48 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ 𝐶 ) )
216 214 215 eqtrd ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
217 216 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑈 = ( Base ‘ 𝐶 ) )
218 212 217 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ∈ 𝑈 )
219 218 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) : 𝑋 ⟶ 𝑈 )
220 202 206 219 4 gsumsubm ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 𝐹 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
221 eqid ⊢ ( .r ‘ 𝐸 ) = ( .r ‘ 𝐸 )
222 4 221 ressmulr ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐹 ) )
223 9 222 syl ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐹 ) )
224 45 48 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝐹 ) = ( ·𝑠 ‘ 𝐶 ) )
225 223 224 eqtr2d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐶 ) = ( .r ‘ 𝐸 ) )
226 225 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ·𝑠 ‘ 𝐶 ) = ( .r ‘ 𝐸 ) )
227 226 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) = ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) )
228 227 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) )
229 228 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) )
230 3 7 10 112 111 13 drgextgsum ⊢ ( 𝜑 → ( 𝐹 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
231 230 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐹 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) = ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
232 220 229 231 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) = ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) )
233 232 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
234 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ Ring )
235 183 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐸 ) )
236 235 208 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
237 216 94 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ⊆ ( Base ‘ 𝐸 ) )
238 121 237 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝐸 ) )
239 238 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑋 ⊆ ( Base ‘ 𝐸 ) )
240 239 72 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ ( Base ‘ 𝐸 ) )
241 eqid ⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
242 eqid ⊢ ( LBasis ‘ 𝐵 ) = ( LBasis ‘ 𝐵 )
243 241 242 lbsss ⊢ ( 𝑌 ∈ ( LBasis ‘ 𝐵 ) → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
244 14 243 syl ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
245 92 94 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐵 ) )
246 244 245 sseqtrrd ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
247 246 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
248 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ 𝑌 )
249 247 248 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
250 35 221 ringass ⊢ ( ( 𝐸 ∈ Ring ∧ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ∧ 𝑗 ∈ ( Base ‘ 𝐸 ) ) ) → ( ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
251 234 236 240 249 250 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
252 251 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
253 252 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) ) )
254 79 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝐸 ∈ Ring )
255 244 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑌 ⊆ ( Base ‘ 𝐵 ) )
256 245 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐵 ) )
257 255 256 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑌 ⊆ ( Base ‘ 𝐸 ) )
258 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 ∈ 𝑌 )
259 257 258 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 ∈ ( Base ‘ 𝐸 ) )
260 35 221 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
261 234 236 240 260 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ∈ ( Base ‘ 𝐸 ) )
262 171 breq2d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ↔ ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ 𝐸 ) ) )
263 262 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ ( Scalar ‘ 𝐶 ) ) ↔ ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ 𝐸 ) ) )
264 20 263 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) finSupp ( 0g ‘ 𝐸 ) )
265 35 254 202 240 185 264 rmfsupp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) finSupp ( 0g ‘ 𝐸 ) )
266 35 81 221 254 202 259 261 265 gsummulc1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ( .r ‘ 𝐸 ) 𝑗 ) ) ) = ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
267 253 266 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) ) = ( ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
268 21 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐿 ‘ 𝑗 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐶 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝐶 ) 𝑖 ) ) ) ( .r ‘ 𝐸 ) 𝑗 ) )
269 233 267 268 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐿 ‘ 𝑗 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) ) )
270 92 94 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) )
271 270 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) )
272 271 oveqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐿 ‘ 𝑗 ) ( .r ‘ 𝐸 ) 𝑗 ) = ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) )
273 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ∈ V )
274 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ V )
275 12 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ) )
276 11 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
277 14 13 273 274 275 276 offval22 ⊢ ( 𝜑 → ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) )
278 277 oveqd ⊢ ( 𝜑 → ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) = ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) 𝑖 ) )
279 278 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) = ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) 𝑖 ) )
280 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ∈ V )
281 eqid ⊢ ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) = ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
282 281 ovmpt4g ⊢ ( ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ∈ V ) → ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) 𝑖 ) = ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
283 248 72 280 282 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑗 ( 𝑗 ∈ 𝑌 , 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) 𝑖 ) = ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) )
284 279 283 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) = ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) )
285 284 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) = ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) ) )
286 285 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ) ) ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) ) ) )
287 269 272 286 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) = ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) ) ) )
288 287 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) = ( 𝑗 ∈ 𝑌 ↦ ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) ) ) ) )
289 288 oveq2d ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) ) ) ) ) )
290 ringcmn ⊢ ( 𝐸 ∈ Ring → 𝐸 ∈ CMnd )
291 79 290 syl ⊢ ( 𝜑 → 𝐸 ∈ CMnd )
292 79 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → 𝐸 ∈ Ring )
293 52 183 eqsstrd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐸 ) )
294 293 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) ⊆ ( Base ‘ 𝐸 ) )
295 simprl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
296 294 295 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑙 ∈ ( Base ‘ 𝐸 ) )
297 simprr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑘 ∈ ( Base ‘ 𝐴 ) )
298 30 37 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
299 298 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
300 297 299 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑘 ∈ ( Base ‘ 𝐸 ) )
301 35 221 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑙 ∈ ( Base ‘ 𝐸 ) ∧ 𝑘 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑙 ( .r ‘ 𝐸 ) 𝑘 ) ∈ ( Base ‘ 𝐸 ) )
302 292 296 300 301 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑘 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑙 ( .r ‘ 𝐸 ) 𝑘 ) ∈ ( Base ‘ 𝐸 ) )
303 35 221 ringcl ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑖 ∈ ( Base ‘ 𝐸 ) ∧ 𝑗 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐸 ) )
304 234 240 249 303 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐸 ) )
305 298 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
306 304 305 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
307 306 anasss ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ) ) → ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
308 307 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) )
309 11 fmpo ⊢ ( ∀ 𝑗 ∈ 𝑌 ∀ 𝑖 ∈ 𝑋 ( 𝑖 ( .r ‘ 𝐸 ) 𝑗 ) ∈ ( Base ‘ 𝐴 ) ↔ 𝐷 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
310 308 309 sylib ⊢ ( 𝜑 → 𝐷 : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐴 ) )
311 inidm ⊢ ( ( 𝑌 × 𝑋 ) ∩ ( 𝑌 × 𝑋 ) ) = ( 𝑌 × 𝑋 )
312 302 76 310 59 59 311 off ⊢ ( 𝜑 → ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) : ( 𝑌 × 𝑋 ) ⟶ ( Base ‘ 𝐸 ) )
313 79 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝐴 ) ) → 𝐸 ∈ Ring )
314 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝐴 ) ) → 𝑢 ∈ ( Base ‘ 𝐴 ) )
315 298 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐴 ) )
316 314 315 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝐴 ) ) → 𝑢 ∈ ( Base ‘ 𝐸 ) )
317 35 221 81 ringlz ⊢ ( ( 𝐸 ∈ Ring ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) → ( ( 0g ‘ 𝐸 ) ( .r ‘ 𝐸 ) 𝑢 ) = ( 0g ‘ 𝐸 ) )
318 313 316 317 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝐴 ) ) → ( ( 0g ‘ 𝐸 ) ( .r ‘ 𝐸 ) 𝑢 ) = ( 0g ‘ 𝐸 ) )
319 59 83 83 76 310 197 318 offinsupp1 ⊢ ( 𝜑 → ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) finSupp ( 0g ‘ 𝐸 ) )
320 35 81 291 14 13 312 319 gsumxp ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) ) = ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( 𝐸 Σg ( 𝑖 ∈ 𝑋 ↦ ( 𝑗 ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) 𝑖 ) ) ) ) ) )
321 30 37 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐴 ) )
322 321 ofeqd ⊢ ( 𝜑 → ∘f ( .r ‘ 𝐸 ) = ∘f ( ·𝑠 ‘ 𝐴 ) )
323 322 oveqd ⊢ ( 𝜑 → ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) = ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) )
324 323 oveq2d ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝐻 ∘f ( .r ‘ 𝐸 ) 𝐷 ) ) = ( 𝐸 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) )
325 289 320 324 3eqtr2rd ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) = ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) )
326 ovexd ⊢ ( 𝜑 → ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ∈ V )
327 15 elfvexd ⊢ ( 𝜑 → 𝐴 ∈ V )
328 1 326 6 327 37 gsumsra ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) = ( 𝐴 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) )
329 325 328 eqtr3d ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑗 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑗 ) ( ·𝑠 ‘ 𝐵 ) 𝑗 ) ) ) = ( 𝐴 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) )
330 18 201 329 3eqtr2d ⊢ ( 𝜑 → 𝑍 = ( 𝐴 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) )
331 200 330 jca ⊢ ( 𝜑 → ( 𝐻 finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑍 = ( 𝐴 Σg ( 𝐻 ∘f ( ·𝑠 ‘ 𝐴 ) 𝐷 ) ) ) )