fedgmullem2 - Mathbox for Thierry Arnoux

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

Theorem fedgmullem2 31026

Description: Lemma for fedgmul 31027 (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‘𝐵))
fedgmullem2.1	⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
fedgmullem2.2	⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (0_g‘𝐴))

**Assertion**
Ref	Expression
fedgmullem2	⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}))

Distinct variable groups: 𝐴,𝑖,𝑗 𝐵,𝑖,𝑗 𝐶,𝑖 𝐷,𝑖,𝑗 𝑖,𝐸,𝑗 𝑈,𝑖 𝑖,𝑊,𝑗 𝑖,𝑋,𝑗 𝑖,𝑌,𝑗 𝜑,𝑖,𝑗 Allowed substitution hints: 𝐶(𝑗) 𝑈(𝑗) 𝐹(𝑖,𝑗) 𝐺(𝑖,𝑗) 𝐻(𝑖,𝑗) 𝐾(𝑖,𝑗) 𝑉(𝑖,𝑗)

Proof of Theorem fedgmullem2 Dummy variables 𝑏 𝑤 𝑘 𝑥 𝑙 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fedgmul.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
2		fedgmul.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ DivRing)
3		fedgmul.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))
4		fedgmul.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))
5		fedgmul.f	. . . . . . . . . . . . . . 15 ⊢ 𝐹 = (𝐸 ↾_s 𝑈)
6	5	subsubrg 19561	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
7	6	biimpa 479	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	3, 4, 7	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
9	8	simpld 497	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
10		fedgmul.a	. . . . . . . . . . . 12 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11		fedgmul.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
12	10, 11	sralvec 30990	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1367	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 19878	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2821	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2821	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 19849	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 19536	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 16555	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 19536	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 19950	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 4006	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 19536	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 19950	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 4007	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3977	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 30989	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 19541	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 30993	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
44	43	oveqdr 7184	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) = (𝑥( ·_𝑠 ‘𝐴)𝑦))
45	3	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
46	8	simprd 498	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
47	46	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈)
48		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49		ressabs 16563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
50	3, 46, 49	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
51	5	oveq1i 7166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
52	50, 51, 11	3eqtr4g 2881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
53	27, 30	srasca 19953	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6674	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 16555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 19953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
59	11, 58	syl5eq 2868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	59, 54	eqtr3d 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6674	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2866	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2916	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝐸) = (._r‘𝐸)
68	67	subrgmcl 19547	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2914	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3191	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2821	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2821	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2821	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2821	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
76		eqid 2821	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 19734	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)))
78	77	biimpar 480	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
79	15, 42, 71, 78	syl12anc 834	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴))
80	20, 32	sseqtrrd 4008	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 20977	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sseldi 3965	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 4007	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾_s 𝑈) = (𝐴 ↾_s 𝑈)
85	84, 74	ressbas2 16555	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
86	83, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
87	32, 86	eqtr3d 2858	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾_s 𝑈)))
88	84, 72	resssca 16650	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
89	3, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
90	60, 89	eqtr3d 2858	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾_s 𝑈)))
91	90	fveq2d 6674	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾_s 𝑈))))
92	90	fveq2d 6674	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘(𝐴 ↾_s 𝑈))))
93		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐸) = (+_g‘𝐸)
94	5, 93	ressplusg 16612	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐸) = (+_g‘𝐹))
95	3, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐹))
96	34, 36	sraaddg 19951	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐴))
97	27, 30	sraaddg 19951	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘𝐶))
98	95, 96, 97	3eqtr3rd 2865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘𝐴))
99		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝐴) = (+_g‘𝐴)
100	84, 99	ressplusg 16612	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
101	3, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
102	98, 101	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘(𝐴 ↾_s 𝑈)))
103	102	oveqdr 7184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+_g‘𝐶)𝑦) = (𝑥(+_g‘(𝐴 ↾_s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2913	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
106		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
107	26, 106	sralvec 30990	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 19878	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
113		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 19651	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
115	114	3expb 1116	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
116	110, 115	sylan 582	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
117		fedgmul.b	. . . . . . . . . . . . . . . . 17 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118	117, 1, 3	drgextvsca 30993	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
119	43, 118	eqtr3d 2858	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
120	5, 67	ressmulr 16625	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (._r‘𝐸) = (._r‘𝐹))
121	3, 120	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (._r‘𝐸) = (._r‘𝐹))
122	26, 104, 4	drgextvsca 30993	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (._r‘𝐹) = ( ·_𝑠 ‘𝐶))
123	121, 118, 122	3eqtr3d 2864	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐶))
124	119, 123	eqtr2d 2857	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐴))
125	84, 75	ressvsca 16651	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
126	3, 125	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
127	124, 126	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
128	127	oveqdr 7184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) = (𝑥( ·_𝑠 ‘(𝐴 ↾_s 𝑈))𝑦))
129		ovexd 7191	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾_s 𝑈) ∈ V)
130	87, 91, 92, 103, 116, 128, 108, 129	lindspropd 30943	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾_s 𝑈)))
131	82, 130	eleqtrd 2915	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)))
132	76, 84	lsslinds 20975	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
133	132	biimpa 479	. . . . . . . . . 10 ⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
134	15, 79, 80, 131, 133	syl31anc 1369	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴))
135		eqid 2821	. . . . . . . . . . 11 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
136		eqid 2821	. . . . . . . . . . 11 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
137	74, 73, 72, 75, 135, 136	islinds5 30932	. . . . . . . . . 10 ⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
138	137	biimpa 479	. . . . . . . . 9 ⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
139	15, 39, 134, 138	syl21anc 835	. . . . . . . 8 ⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
140	139	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
141		eqid 2821	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
142		fvexd 6685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) ∈ V)
143		fedgmullem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
144	143	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵))
145	16	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
146		fedgmullem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
147		fvexd 6685	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
148	143, 16	xpexd 7474	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
149		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
150		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
151	149, 73, 136, 150	frlmelbas 20900	. . . . . . . . . . . . . . . 16 ⊢ (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴)))))
152	147, 148, 151	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴)))))
153	146, 152	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴))))
154	153	simpld 497	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)))
155		fvexd 6685	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
156	155, 148	elmapd 8420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
157	154, 156	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
158	157	ffnd 6515	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
159	158	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
160		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
161	153	simprd 498	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0_g‘(Scalar‘𝐴)))
162		drngring 19509	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
163	1, 162	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
164		ringmnd 19306	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
165	163, 164	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
166		subrgsubg 19541	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
167	9, 166	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
168		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
169	168	subg0cl 18287	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ 𝑉)
170	167, 169	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑉)
171	46, 170	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑈)
172	5, 21, 168	ress0g 17939	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐹))
173	165, 171, 23, 172	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐹))
174	54	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐾) = (0_g‘(Scalar‘𝐶)))
175	11, 168	subrg0 19542	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0_g‘𝐸) = (0_g‘𝐾))
176	9, 175	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐾))
177	60	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐶)))
178	174, 176, 177	3eqtr4d 2866	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘(Scalar‘𝐴)))
179	173, 178	eqtr3d 2858	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
180	161, 179	breqtrrd 5094	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0_g‘𝐹))
181	180	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0_g‘𝐹))
182	141, 142, 144, 145, 159, 160, 181	fsuppcurry1 30461	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘𝐹))
183	179	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
184	182, 183	breqtrd 5092	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)))
185		eqidd 2822	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
186	157	fovrnda 7319	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	186	anassrs 470	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
188	185, 187	fvmpt2d 6781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
189	188	oveq1d 7171	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
190	119	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
191	190	oveqd 7173	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
192	189, 191	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
193	192	mpteq2dva 5161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
194	193	oveq2d 7172	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
195	1	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing)
196	9	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸))
197	2	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing)
198	10, 195, 196, 11, 197, 145	drgextgsum 30997	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
199	3	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
200	104	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
201	117, 195, 199, 5, 200, 145	drgextgsum 30997	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
202	198, 201	eqtr3d 2858	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
203	194, 202	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
204	143	mptexd 6987	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ V)
205		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘𝐵) = (0_g‘𝐵)
206	117, 5	sralvec 30990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
207	1, 104, 3, 206	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
208		lveclmod 19878	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
209	207, 208	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
210	209	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
211		lmodabl 19681	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
213	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
214	213, 3, 23	srasubrg 30989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
215		subrgsubg 19541	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
216	214, 215	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵))
217	216	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
218	110	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
219	61	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
220	187, 219	eleqtrd 2915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
221	20	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
222		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
223	221, 222	sseldd 3968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
224	17, 111, 112, 113	lmodvscl 19651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	218, 220, 223, 224	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
226	123	oveqd 7173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
227	226	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
228	32	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
229	225, 227, 228	3eltr4d 2928	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) ∈ 𝑈)
230	229	fmpttd 6879	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
231	213, 23	srasca 19953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
232	5, 231	syl5eq 2868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
233	232	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
234		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
235		ovexd 7191	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
236	20, 33	sstrd 3977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
237	236	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
238		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
239	237, 238	sseldd 3968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
240	239	anassrs 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
241	213, 23	srabase 19950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
242	241	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
243	240, 242	eleqtrd 2915	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
244		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
245		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
246	145, 210, 233, 234, 235, 243, 205, 244, 245, 182	mptscmfsupp0 19699	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) finSupp (0_g‘𝐵))
247	205, 212, 145, 217, 230, 246	gsumsubgcl 19040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
248	232	fveq2d 6674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
249	25, 248	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
250	249	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
251	247, 250	eleqtrd 2915	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
252	251	fmpttd 6879	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
253	252	ffund 6518	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
254		fvexd 6685	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) ∈ V)
255		fconstmpt 5614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0_g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
256	255	eqeq2i 2834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
257		ovex 7189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
258	257	rgenw 3150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
259		mpteqb 6787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
260	258, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
261	256, 260	bitri 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
262	261	necon3abii 3062	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
263		df-ov 7159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
264	263	eqcomi 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
265	264	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
266	265	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0_g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
267	266	necon3abid 3052	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
268	267	rexbidva 3296	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
269		rexnal 3238	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
270	268, 269	syl6rbb 290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
271	262, 270	syl5bb 285	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
272	271	rabbidva 3478	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))})
273		fveq2 6670	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
274	273	neeq1d 3075	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
275	274	dmrab 30260	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))}
276	272, 275	syl6eqr 2874	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
277		fvexd 6685	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) ∈ V)
278		suppvalfn 7837	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0_g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
279	158, 148, 277, 278	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
280	161	fsuppimpd 8840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) ∈ Fin)
281	279, 280	eqeltrrd 2914	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
282		dmfi 8802	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
283	281, 282	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
284	276, 283	eqeltrd 2913	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ∈ Fin)
285		nfv 1915	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
286		nfcv 2977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
287		nfmpt1 5164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
288		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0_g‘(Scalar‘𝐴))})
289	287, 288	nfne 3119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})
290	289, 286	nfrabw 3385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}
291	286, 290	nfdif 4102	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
292	291	nfcriv 2967	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
293	285, 292	nfan 1900	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
294		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
295	294	eldifad 3948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
296	294	eldifbd 3949	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
297		oveq1 7163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
298	297	mpteq2dv 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
299	298	neeq1d 3075	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
300	299	elrab 3680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
301	296, 300	sylnib 330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
302	295, 301	mpnanrd 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}))
303		nne 3020	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
304	302, 303	sylib 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
305	304, 255	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
306		ovex 7189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
307	306	rgenw 3150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
308		mpteqb 6787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
309	307, 308	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
310	305, 309	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
311	310	r19.21bi 3208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
312	311	oveq1d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖))
313	117, 1, 3	drgext0g 30992	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐵))
314	117, 1, 3	drgext0gsca 30994	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
315	313, 178, 314	3eqtr3d 2864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
316	315	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
317	316	oveq1d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖))
318	209	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod)
319	295, 243	syldanl 603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
320		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
321		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
322	234, 320, 245, 321, 205	lmod0vs 19667	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
323	318, 319, 322	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
324	312, 317, 323	3eqtrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
325	293, 324	mpteq2da 5160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵)))
326	325	oveq2d 7172	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))))
327	209, 211	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ Abel)
328		ablgrp 18911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
329		grpmnd 18110	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
330	327, 328, 329	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
331	205	gsumz 18000	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
332	330, 16, 331	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
333	332	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
334	314	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
335	326, 333, 334	3eqtrd 2860	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
336	335, 143	suppss2 7864	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) supp (0_g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
337		suppssfifsupp 8848	. . . . . . . . . . . . . 14 ⊢ ((((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ V ∧ Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∧ (0_g‘(Scalar‘𝐵)) ∈ V) ∧ ({𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ∈ Fin ∧ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) supp (0_g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)))
338	204, 253, 254, 284, 336, 337	syl32anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)))
339		eqidd 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
340		ovexd 7191	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V)
341	339, 340	fvmpt2d 6781	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
342	341	oveq1d 7171	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
343	342	mpteq2dva 5161	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
344	343	oveq2d 7172	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
345	119	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
346	43	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
347	346	oveqd 7173	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
348	347	mpteq2dva 5161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))
349	118	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
350	349	oveqd 7173	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
351	350	mpteq2dv 5162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
352	348, 351	eqtr3d 2858	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
353	352	oveq2d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
354		eqidd 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
355	345, 353, 354	oveq123d 7177	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
356	202	oveq1d 7171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
357	355, 356	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
358	357	mpteq2dva 5161	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
359	358	oveq2d 7172	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
360	10, 21	sraring 30987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
361	163, 36, 360	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
362		ringcmn 19331	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
363	361, 362	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
364	163	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
365		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
366	234, 365	lbsss 19849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
367	143, 366	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
368	367, 241	sseqtrrd 4008	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
369	368	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
370		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
371	369, 370	sseldd 3968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
372	21, 67	ringcl 19311	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
373	364, 239, 371, 372	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
374	37	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴))
375	373, 374	eleqtrd 2915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
376	375	ralrimivva 3191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
377		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗))
378	377	fmpo 7766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
379	376, 378	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
380	72, 73, 75, 74, 15, 157, 379, 148	lcomf 19673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
381	72, 73, 75, 74, 15, 157, 379, 148, 135, 136, 161	lcomfsupp 19674	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) finSupp (0_g‘𝐴))
382	74, 135, 363, 143, 16, 380, 381	gsumxp 19096	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))))
383		fedgmullem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (0_g‘𝐴))
384	163	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
385	157	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
386	57, 55	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
387	386, 36	eqsstrrd 4006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
388	61, 387	eqsstrd 4005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
389	388, 37	sseqtrd 4007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390	389	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
391	385, 390	fssd 6528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
392		simp2 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
393		simp3 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
394	391, 392, 393	fovrnd 7320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
395	37	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
396	394, 395	eleqtrrd 2916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
397	239	3impb 1111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
398	371	3impb 1111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
399	21, 67	ringass 19314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
400	384, 396, 397, 398, 399	syl13anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
401	400	mpoeq3dva 7231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
402		ovexd 7191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
403		ovexd 7191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(._r‘𝐸)𝑗) ∈ V)
404		fnov 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
405	158, 404	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
406	377	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗)))
407	143, 16, 402, 403, 405, 406	offval22 7783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
408		ofeq 7411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((._r‘𝐸) = ( ·_𝑠 ‘𝐴) → ∘_f (._r‘𝐸) = ∘_f ( ·_𝑠 ‘𝐴))
409	43, 408	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘_f (._r‘𝐸) = ∘_f ( ·_𝑠 ‘𝐴))
410	409	oveqd 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷))
411	401, 407, 410	3eqtr2rd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
412	411	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
413	412	oveqd 7173	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖))
414		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
415		ovexd 7191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V)
416		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
417	416	ovmpt4g 7297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
418	414, 222, 415, 417	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
419	413, 418	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
420	419	mpteq2dva 5161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
421	420	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))))
422	163	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
423	368	sselda 3967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
424	163	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
425	387	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
426	425, 220	sseldd 3968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
427	21, 67	ringcl 19311	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
428	424, 426, 240, 427	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
429	313	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐸) = (0_g‘𝐵))
430	246, 351, 429	3brtr4d 5098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) finSupp (0_g‘𝐸))
431	21, 168, 93, 67, 422, 145, 423, 428, 430	gsummulc1 19356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
432	421, 431	eqtrd 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
433	145	mptexd 6987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
434	15	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
435	36	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
436	10, 433, 195, 434, 435	gsumsra 30685	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))
437	145	mptexd 6987	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) ∈ V)
438	10, 437, 195, 434, 435	gsumsra 30685	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))))
439	438	oveq1d 7171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
440	43	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
441	348	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))))
442	440, 441, 354	oveq123d 7177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
443	439, 442	eqtrd 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
444	432, 436, 443	3eqtr3d 2864	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
445	444	mpteq2dva 5161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)))
446	445	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))))
447	382, 383, 446	3eqtr3rd 2865	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐴))
448	10, 1, 9	drgext0g 30992	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐴))
449	447, 448, 313	3eqtr2d 2862	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐵))
450	10, 1, 9, 11, 2, 143	drgextgsum 30997	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
451	117, 1, 3, 5, 104, 143	drgextgsum 30997	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
452	450, 451	eqtr3d 2858	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
453	359, 449, 452	3eqtr3rd 2865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
454	344, 453	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
455		breq1 5069	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0_g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵))))
456		nfmpt1 5164	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
457	456	nfeq2 2995	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
458		fveq1 6669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗))
459	458	oveq1d 7171	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
460	459	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
461	457, 460	mpteq2da 5160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
462	461	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
463	462	eqeq1d 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵) ↔ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)))
464	455, 463	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))))
465		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
466	464, 465	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})) ↔ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))}))))
467	365	lbslinds 20977	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
468	467, 143	sseldi 3965	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
469		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
470	234, 469, 320, 245, 205, 321	islinds5 30932	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}))))
471	470	biimpa 479	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
472	209, 367, 468, 471	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
473		fvexd 6685	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
474		elmapg 8419	. . . . . . . . . . . . . . . 16 ⊢ (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
475	474	biimpar 480	. . . . . . . . . . . . . . 15 ⊢ ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
476	473, 143, 252, 475	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
477	466, 472, 476	rspcdva 3625	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
478	338, 454, 477	mp2and 697	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))}))
479		fconstmpt 5614	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0_g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵)))
480	478, 479	syl6eq 2872	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))))
481		ovex 7189	. . . . . . . . . . . . 13 ⊢ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
482	481	rgenw 3150	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
483		mpteqb 6787	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵))))
484	482, 483	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
485	480, 484	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
486	485	r19.21bi 3208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
487	313, 448, 314	3eqtr3rd 2865	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
488	487	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
489	203, 486, 488	3eqtrd 2860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))
490	184, 489	jca 514	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
491	187	fmpttd 6879	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
492		fvexd 6685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
493	492, 145	elmapd 8420	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
494	491, 493	mpbird 259	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋))
495		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
496	495	breq1d 5076	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴))))
497		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
498		nfmpt1 5164	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
499	498	nfeq2 2995	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
500	497, 499	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
501		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
502	501	fveq1d 6672	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
503	502	oveq1d 7171	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))
504	500, 503	mpteq2da 5160	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)))
505	504	oveq2d 7172	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))))
506	505	eqeq1d 2823	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴) ↔ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
507	496, 506	anbi12d 632	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))))
508	495	eqeq1d 2823	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
509	507, 508	imbi12d 347	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
510	494, 509	rspcdv 3615	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
511	140, 490, 510	mp2d 49	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
512	511, 255	syl6eq 2872	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
513	512, 309	sylib 220	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
514	513	ralrimiva 3182	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
515		eqidd 2822	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴)))
516		fvexd 6685	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
517		fvexd 6685	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
518	158, 515, 516, 517	fnmpoovd 7782	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
519	514, 518	mpbird 259	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
520		fconstmpo 7269	. 2 ⊢ ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
521	519, 520	syl6eqr 2874	1 ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3494 ∖ cdif 3933 ⊆ wss 3936 {csn 4567 ⟨cop 4573 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 dom cdm 5555 Fun wfun 6349 Fn wfn 6350 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ∈ cmpo 7158 ∘_f cof 7407 supp csupp 7830 ↑_m cmap 8406 Fincfn 8509 finSupp cfsupp 8833 Basecbs 16483 ↾_s cress 16484 +_gcplusg 16565 ._rcmulr 16566 Scalarcsca 16568 ·_𝑠 cvsca 16569 0_gc0g 16713 Σ_g cgsu 16714 Mndcmnd 17911 Grpcgrp 18103 SubGrpcsubg 18273 CMndccmn 18906 Abelcabl 18907 Ringcrg 19297 DivRingcdr 19502 SubRingcsubrg 19531 LModclmod 19634 LSubSpclss 19703 LBasisclbs 19846 LVecclvec 19874 subringAlg csra 19940 freeLMod cfrlm 20890 LIndSclinds 20949

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-oadd 8106 df-er 8289 df-map 8408 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-sup 8906 df-oi 8974 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-fz 12894 df-fzo 13035 df-seq 13371 df-hash 13692 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-hom 16589 df-cco 16590 df-0g 16715 df-gsum 16716 df-prds 16721 df-pws 16723 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-mhm 17956 df-submnd 17957 df-grp 18106 df-minusg 18107 df-sbg 18108 df-mulg 18225 df-subg 18276 df-ghm 18356 df-cntz 18447 df-cmn 18908 df-abl 18909 df-mgp 19240 df-ur 19252 df-ring 19299 df-drng 19504 df-subrg 19533 df-lmod 19636 df-lss 19704 df-lsp 19744 df-lmhm 19794 df-lbs 19847 df-lvec 19875 df-sra 19944 df-rgmod 19945 df-nzr 20031 df-dsmm 20876 df-frlm 20891 df-uvc 20927 df-lindf 20950 df-linds 20951

This theorem is referenced by: fedgmul 31027

W3C validator