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 33787

Description: Lemma for fedgmul 33788. (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 20531	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
7	6	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	3, 4, 7	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
9	8	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
10		fedgmul.a	. . . . . . . . . . . 12 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11		fedgmul.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
12	10, 11	sralvec 33741	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 21058	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2736	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 21029	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 20505	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 17165	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 20505	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 21129	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 3969	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 20505	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 21129	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 3970	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3944	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 33740	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 20510	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 33747	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
44	43	oveqdr 7386	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) = (𝑥( ·_𝑠 ‘𝐴)𝑦))
45	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
46	8	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
47	46	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈)
48		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49		ressabs 17175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
50	3, 46, 49	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
51	5	oveq1i 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
52	50, 51, 11	3eqtr4g 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
53	27, 30	srasca 21132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 17165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 21132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
59	11, 58	eqtrid 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	52, 53, 59	3eqtr3rd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝐸) = (._r‘𝐸)
68	67	subrgmcl 20517	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2837	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3179	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2736	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2736	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2736	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2736	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
76		eqid 2736	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 20913	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)))
78	77	biimpar 477	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
79	15, 42, 71, 78	syl12anc 836	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴))
80	20, 32	sseqtrrd 3971	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 21788	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sselid 3931	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 3970	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾_s 𝑈) = (𝐴 ↾_s 𝑈)
85	84, 74	ressbas2 17165	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
86	83, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
87	25, 86, 31	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾_s 𝑈)))
88	84, 72	resssca 17263	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
89	3, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
90	60, 89	eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾_s 𝑈)))
91	90	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾_s 𝑈))))
92	90	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘(𝐴 ↾_s 𝑈))))
93		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐸) = (+_g‘𝐸)
94	5, 93	ressplusg 17211	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐸) = (+_g‘𝐹))
95	3, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐹))
96	34, 36	sraaddg 21130	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐴))
97	27, 30	sraaddg 21130	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘𝐶))
98	95, 96, 97	3eqtr3rd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘𝐴))
99		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝐴) = (+_g‘𝐴)
100	84, 99	ressplusg 17211	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
101	3, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
102	98, 101	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘(𝐴 ↾_s 𝑈)))
103	102	oveqdr 7386	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+_g‘𝐶)𝑦) = (𝑥(+_g‘(𝐴 ↾_s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
106		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
107	26, 106	sralvec 33741	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 21058	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
113		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 20829	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
115	114	3expb 1120	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
116	110, 115	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
117		fedgmul.b	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118	117, 1, 3	drgextvsca 33747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
119	43, 118	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
120	84, 75	ressvsca 17264	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
121	3, 120	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
122	5, 67	ressmulr 17227	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (._r‘𝐸) = (._r‘𝐹))
123	3, 122	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = (._r‘𝐹))
124	26, 104, 4	drgextvsca 33747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐹) = ( ·_𝑠 ‘𝐶))
125	123, 118, 124	3eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐶))
126	119, 121, 125	3eqtr3rd 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
127	126	oveqdr 7386	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) = (𝑥( ·_𝑠 ‘(𝐴 ↾_s 𝑈))𝑦))
128		ovexd 7393	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾_s 𝑈) ∈ V)
129	87, 91, 92, 103, 116, 127, 108, 128	lindspropd 33464	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾_s 𝑈)))
130	82, 129	eleqtrd 2838	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)))
131	76, 84	lsslinds 21786	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132	131	biimpa 476	. . . . . . . . . 10 ⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
133	15, 79, 80, 130, 132	syl31anc 1375	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴))
134		eqid 2736	. . . . . . . . . . 11 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
135		eqid 2736	. . . . . . . . . . 11 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
136	74, 73, 72, 75, 134, 135	islinds5 33448	. . . . . . . . . 10 ⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
137	136	biimpa 476	. . . . . . . . 9 ⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
138	15, 39, 133, 137	syl21anc 837	. . . . . . . 8 ⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
139	138	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
140		eqid 2736	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
141		fvexd 6849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) ∈ V)
142		fedgmullem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
143	142	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵))
144	16	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145		fedgmullem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146		fvexd 6849	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
147	142, 16	xpexd 7696	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
148		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150	148, 73, 135, 149	frlmelbas 21711	. . . . . . . . . . . . . . . 16 ⊢ (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴)))))
151	146, 147, 150	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴)))))
152	145, 151	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴))))
153	152	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)))
154		fvexd 6849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155	154, 147	elmapd 8777	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156	153, 155	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157	156	ffnd 6663	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
158	157	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
160	152	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0_g‘(Scalar‘𝐴)))
161		drngring 20669	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
162	1, 161	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
163		ringmnd 20178	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164	162, 163	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
165		subrgsubg 20510	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
166	9, 165	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
167		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
168	167	subg0cl 19064	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ 𝑉)
169	166, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑉)
170	46, 169	sseldd 3934	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑈)
171	5, 21, 167	ress0g 18687	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐹))
172	164, 170, 23, 171	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐹))
173	54	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐾) = (0_g‘(Scalar‘𝐶)))
174	11, 167	subrg0 20512	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0_g‘𝐸) = (0_g‘𝐾))
175	9, 174	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐾))
176	60	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐶)))
177	173, 175, 176	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘(Scalar‘𝐴)))
178	172, 177	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
179	160, 178	breqtrrd 5126	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0_g‘𝐹))
180	179	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0_g‘𝐹))
181	140, 141, 143, 144, 158, 159, 180	fsuppcurry1 32803	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘𝐹))
182	178	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
183	181, 182	breqtrd 5124	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)))
184		eqidd 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
185	156	fovcdmda 7529	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186	185	anassrs 467	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	184, 186	fvmpt2d 6954	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188	187	oveq1d 7373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
189	119	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
190	189	oveqd 7375	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
191	188, 190	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
192	191	mpteq2dva 5191	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
193	192	oveq2d 7374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
194	1	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing)
195	9	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸))
196	2	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing)
197	10, 194, 195, 11, 196, 144	drgextgsum 33751	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
198	3	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199	104	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
200	117, 194, 198, 5, 199, 144	drgextgsum 33751	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
201	197, 200	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
202	193, 201	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
203	142	mptexd 7170	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ V)
204		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘𝐵) = (0_g‘𝐵)
205	117, 5	sralvec 33741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
206	1, 104, 3, 205	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
207		lveclmod 21058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208	206, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
209	208	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
210		lmodabl 20860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
212	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213	212, 3, 23	srasubrg 33740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
214		subrgsubg 20510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵))
216	215	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217	110	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
218	61	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219	186, 218	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
220	20	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
221		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
222	220, 221	sseldd 3934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
223	17, 111, 112, 113	lmodvscl 20829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
224	217, 219, 222, 223	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	125	oveqd 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
226	225	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
227	32	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
228	224, 226, 227	3eltr4d 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) ∈ 𝑈)
229	228	fmpttd 7060	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
230	212, 23	srasca 21132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
231	5, 230	eqtrid 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
232	231	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
233		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
234		ovexd 7393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
235	20, 33	sstrd 3944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
236	235	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
238	236, 237	sseldd 3934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
239	238	anassrs 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
240	212, 23	srabase 21129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241	240	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
242	239, 241	eleqtrd 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
243		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
244		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
245	144, 209, 232, 233, 234, 242, 204, 243, 244, 181	mptscmfsupp0 20878	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) finSupp (0_g‘𝐵))
246	204, 211, 144, 216, 229, 245	gsumsubgcl 19849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
247	231	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
248	25, 247	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
249	248	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250	246, 249	eleqtrd 2838	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251	250	fmpttd 7060	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252	251	ffund 6666	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
253		fvexd 6849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) ∈ V)
254		fconstmpt 5686	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0_g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
255	254	eqeq2i 2749	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
256		ovex 7391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
257	256	rgenw 3055	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
258		mpteqb 6960	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
259	257, 258	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
260	255, 259	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
261	260	necon3abii 2978	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
262		df-ov 7361	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263	262	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265	264	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0_g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
266	265	necon3abid 2968	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
267	266	rexbidva 3158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
268		rexnal 3088	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
269	267, 268	bitr2di 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
270	261, 269	bitrid 283	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
271	270	rabbidva 3405	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))})
272		fveq2 6834	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273	272	neeq1d 2991	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
274	273	dmrab 32571	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))}
275	271, 274	eqtr4di 2789	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
276		fvexd 6849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) ∈ V)
277		suppvalfn 8110	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0_g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
278	157, 147, 276, 277	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
279	160	fsuppimpd 9272	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) ∈ Fin)
280	278, 279	eqeltrrd 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
281		dmfi 9235	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
282	280, 281	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
283	275, 282	eqeltrd 2836	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ∈ Fin)
284		nfv 1915	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
285		nfcv 2898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
286		nfmpt1 5197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
287		nfcv 2898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0_g‘(Scalar‘𝐴))})
288	286, 287	nfne 3033	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})
289	288, 285	nfrabw 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}
290	285, 289	nfdif 4081	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
291	290	nfcri 2890	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
292	284, 291	nfan 1900	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
293		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
294	293	eldifad 3913	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
295	293	eldifbd 3914	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
296		oveq1 7365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297	296	mpteq2dv 5192	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
298	297	neeq1d 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
299	298	elrab 3646	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
300	295, 299	sylnib 328	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
301	294, 300	mpnanrd 409	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}))
302		nne 2936	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
303	301, 302	sylib 218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
304	303, 254	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
305		ovex 7391	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
306	305	rgenw 3055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
307		mpteqb 6960	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
308	306, 307	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
309	304, 308	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
310	309	r19.21bi 3228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
311	310	oveq1d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖))
312	117, 1, 3	drgext0g 33746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐵))
313	117, 1, 3	drgext0gsca 33748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
314	312, 177, 313	3eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
315	314	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
316	315	oveq1d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖))
317	208	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod)
318	294, 242	syldanl 602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
319		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
320		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
321	233, 319, 244, 320, 204	lmod0vs 20846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
322	317, 318, 321	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
323	311, 316, 322	3eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
324	292, 323	mpteq2da 5190	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵)))
325	324	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))))
326		ablgrp 19714	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
327		grpmnd 18870	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
328	208, 210, 326, 327	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
329	204	gsumz 18761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
330	328, 16, 329	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
331	330	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
332	313	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
333	325, 331, 332	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
334	333, 142	suppss2 8142	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) supp (0_g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
335		suppssfifsupp 9283	. . . . . . . . . . . . . 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‘𝐵)))
336	203, 252, 253, 283, 334, 335	syl32anc 1380	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)))
337		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
338		ovexd 7393	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V)
339	337, 338	fvmpt2d 6954	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
340	339	oveq1d 7373	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
341	340	mpteq2dva 5191	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
342	341	oveq2d 7374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
343	119	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
344	43	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
345	344	oveqd 7375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
346	345	mpteq2dva 5191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))
347	118	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
348	347	oveqd 7375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
349	348	mpteq2dv 5192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
350	346, 349	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
351	350	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
352		eqidd 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
353	343, 351, 352	oveq123d 7379	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
354	201	oveq1d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
355	353, 354	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
356	355	mpteq2dva 5191	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
357	356	oveq2d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
358	10, 21	sraring 21138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
359	162, 36, 358	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
360		ringcmn 20217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
361	359, 360	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
362	162	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
363		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
364	233, 363	lbsss 21029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
365	142, 364	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
366	365, 240	sseqtrrd 3971	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
367	366	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
368		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
369	367, 368	sseldd 3934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
370	21, 67	ringcl 20185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
371	362, 238, 369, 370	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
372	37	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴))
373	371, 372	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
374	373	ralrimivva 3179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
375		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗))
376	375	fmpo 8012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
377	374, 376	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378	72, 73, 75, 74, 15, 156, 377, 147	lcomf 20852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
379	72, 73, 75, 74, 15, 156, 377, 147, 134, 135, 160	lcomfsupp 20853	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) finSupp (0_g‘𝐴))
380	74, 134, 361, 142, 16, 378, 379	gsumxp 19905	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))))
381		fedgmullem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (0_g‘𝐴))
382	162	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
383	156	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
384	57, 55	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
385	384, 36	eqsstrrd 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
386	61, 385	eqsstrd 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
387	386, 37	sseqtrd 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
388	387	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389	383, 388	fssd 6679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
390		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
391		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
392	389, 390, 391	fovcdmd 7530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
393	37	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
394	392, 393	eleqtrrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
395	238	3impb 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
396	369	3impb 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
397	21, 67	ringass 20188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
398	382, 394, 395, 396, 397	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
399	398	mpoeq3dva 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
400		ovexd 7393	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
401		ovexd 7393	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(._r‘𝐸)𝑗) ∈ V)
402		fnov 7489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
403	157, 402	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
404	375	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗)))
405	142, 16, 400, 401, 403, 404	offval22 8030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
406	43	ofeqd 7624	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘_f (._r‘𝐸) = ∘_f ( ·_𝑠 ‘𝐴))
407	406	oveqd 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷))
408	399, 405, 407	3eqtr2rd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
409	408	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
410	409	oveqd 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖))
411		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
412		ovexd 7393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V)
413		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
414	413	ovmpt4g 7505	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
415	411, 221, 412, 414	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
416	410, 415	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
417	416	mpteq2dva 5191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
418	417	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))))
419	162	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
420	366	sselda 3933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
421	162	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
422	385	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
423	422, 219	sseldd 3934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
424	21, 67	ringcl 20185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
425	421, 423, 239, 424	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
426	312	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐸) = (0_g‘𝐵))
427	245, 349, 426	3brtr4d 5130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) finSupp (0_g‘𝐸))
428	21, 167, 67, 419, 144, 420, 425, 427	gsummulc1 20251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
429	418, 428	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
430	144	mptexd 7170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
431	15	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
432	36	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
433	10, 430, 194, 431, 432	gsumsra 33130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))
434	144	mptexd 7170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) ∈ V)
435	10, 434, 194, 431, 432	gsumsra 33130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))))
436	435	oveq1d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
437	43	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
438	346	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))))
439	437, 438, 352	oveq123d 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
440	436, 439	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
441	429, 433, 440	3eqtr3d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
442	441	mpteq2dva 5191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)))
443	442	oveq2d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))))
444	380, 381, 443	3eqtr3rd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐴))
445	10, 1, 9	drgext0g 33746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐴))
446	444, 445, 312	3eqtr2d 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐵))
447	10, 1, 9, 11, 2, 142	drgextgsum 33751	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
448	117, 1, 3, 5, 104, 142	drgextgsum 33751	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
449	447, 448	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
450	357, 446, 449	3eqtr3rd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
451	342, 450	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
452		breq1 5101	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0_g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵))))
453		nfmpt1 5197	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
454	453	nfeq2 2916	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
455		fveq1 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗))
456	455	oveq1d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
457	456	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
458	454, 457	mpteq2da 5190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
459	458	oveq2d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
460	459	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵) ↔ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)))
461	452, 460	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))))
462		eqeq1 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
463	461, 462	imbi12d 344	. . . . . . . . . . . . . 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‘𝐵))}))))
464	363	lbslinds 21788	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
465	464, 142	sselid 3931	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
466		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
467	233, 466, 319, 244, 204, 320	islinds5 33448	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}))))
468	467	biimpa 476	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
469	208, 365, 465, 468	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
470		fvexd 6849	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
471		elmapg 8776	. . . . . . . . . . . . . . . 16 ⊢ (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
472	471	biimpar 477	. . . . . . . . . . . . . . 15 ⊢ ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
473	470, 142, 251, 472	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
474	463, 469, 473	rspcdva 3577	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
475	336, 451, 474	mp2and 699	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))}))
476		fconstmpt 5686	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0_g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵)))
477	475, 476	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))))
478		ovex 7391	. . . . . . . . . . . . 13 ⊢ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
479	478	rgenw 3055	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
480		mpteqb 6960	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵))))
481	479, 480	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
482	477, 481	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
483	482	r19.21bi 3228	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
484	312, 445, 313	3eqtr3rd 2780	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
485	484	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
486	202, 483, 485	3eqtrd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))
487	183, 486	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
488	186	fmpttd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
489		fvexd 6849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
490	489, 144	elmapd 8777	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
491	488, 490	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋))
492		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
493	492	breq1d 5108	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴))))
494		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
495		nfmpt1 5197	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
496	495	nfeq2 2916	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
497	494, 496	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
498		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
499	498	fveq1d 6836	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
500	499	oveq1d 7373	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))
501	497, 500	mpteq2da 5190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)))
502	501	oveq2d 7374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))))
503	502	eqeq1d 2738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴) ↔ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
504	493, 503	anbi12d 632	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))))
505	492	eqeq1d 2738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
506	504, 505	imbi12d 344	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
507	491, 506	rspcdv 3568	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
508	139, 487, 507	mp2d 49	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
509	508, 254	eqtrdi 2787	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
510	509, 308	sylib 218	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
511	510	ralrimiva 3128	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
512		eqidd 2737	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴)))
513		fvexd 6849	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
514		fvexd 6849	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
515	157, 512, 513, 514	fnmpoovd 8029	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
516	511, 515	mpbird 257	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
517		fconstmpo 7475	. 2 ⊢ ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
518	516, 517	eqtr4di 2789	1 ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3399 Vcvv 3440 ∖ cdif 3898 ⊆ wss 3901 {csn 4580 ⟨cop 4586 class class class wbr 5098 ↦ cmpt 5179 × cxp 5622 dom cdm 5624 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ∈ cmpo 7360 ∘_f cof 7620 supp csupp 8102 ↑_m cmap 8763 Fincfn 8883 finSupp cfsupp 9264 Basecbs 17136 ↾_s cress 17157 +_gcplusg 17177 ._rcmulr 17178 Scalarcsca 17180 ·_𝑠 cvsca 17181 0_gc0g 17359 Σ_g cgsu 17360 Mndcmnd 18659 Grpcgrp 18863 SubGrpcsubg 19050 CMndccmn 19709 Abelcabl 19710 Ringcrg 20168 SubRingcsubrg 20502 DivRingcdr 20662 LModclmod 20811 LSubSpclss 20882 LBasisclbs 21026 LVecclvec 21054 subringAlg csra 21123 freeLMod cfrlm 21701 LIndSclinds 21760

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-map 8765 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-sup 9345 df-oi 9415 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-fz 13424 df-fzo 13571 df-seq 13925 df-hash 14254 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-hom 17201 df-cco 17202 df-0g 17361 df-gsum 17362 df-prds 17367 df-pws 17369 df-mre 17505 df-mrc 17506 df-acs 17508 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mhm 18708 df-submnd 18709 df-grp 18866 df-minusg 18867 df-sbg 18868 df-mulg 18998 df-subg 19053 df-ghm 19142 df-cntz 19246 df-cmn 19711 df-abl 19712 df-mgp 20076 df-rng 20088 df-ur 20117 df-ring 20170 df-nzr 20446 df-subrng 20479 df-subrg 20503 df-drng 20664 df-lmod 20813 df-lss 20883 df-lsp 20923 df-lmhm 20974 df-lbs 21027 df-lvec 21055 df-sra 21125 df-rgmod 21126 df-dsmm 21687 df-frlm 21702 df-uvc 21738 df-lindf 21761 df-linds 21762

This theorem is referenced by: fedgmul 33788

W3C validator