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 34315

Description: Lemma for fedgmul 34316. (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 20862	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
7	6	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	3, 4, 7	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
9	8	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
10		fedgmul.a	. . . . . . . . . . . 12 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11		fedgmul.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
12	10, 11	sralvec 34270	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 21393	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2763	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2763	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 21364	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 20836	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 17428	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 20836	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 21464	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 3947	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 20836	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 21464	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 3948	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3922	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 34269	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 20841	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 34276	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
44	43	oveqdr 7455	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) = (𝑥( ·_𝑠 ‘𝐴)𝑦))
45	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
46	8	simprd 501	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
47	46	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈)
48		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49		ressabs 17438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
50	3, 46, 49	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
51	5	oveq1i 7437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
52	50, 51, 11	3eqtr4g 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
53	27, 30	srasca 21467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 17428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 21467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
59	11, 58	eqtrid 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	52, 53, 59	3eqtr3rd 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2808	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2866	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3913	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝐸) = (._r‘𝐸)
68	67	subrgmcl 20848	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3208	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2763	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2763	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2763	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2763	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
76		eqid 2763	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 21249	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)))
78	77	biimpar 483	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
79	15, 42, 71, 78	syl12anc 850	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴))
80	20, 32	sseqtrrd 3949	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 22151	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sselid 3910	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 3948	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾_s 𝑈) = (𝐴 ↾_s 𝑈)
85	84, 74	ressbas2 17428	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
86	83, 85	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
87	25, 86, 31	3eqtr3rd 2807	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾_s 𝑈)))
88	84, 72	resssca 17526	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
89	3, 88	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
90	60, 89	eqtr3d 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾_s 𝑈)))
91	90	fveq2d 6897	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾_s 𝑈))))
92	90	fveq2d 6897	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘(𝐴 ↾_s 𝑈))))
93		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐸) = (+_g‘𝐸)
94	5, 93	ressplusg 17474	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐸) = (+_g‘𝐹))
95	3, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐹))
96	34, 36	sraaddg 21465	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐴))
97	27, 30	sraaddg 21465	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘𝐶))
98	95, 96, 97	3eqtr3rd 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘𝐴))
99		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝐴) = (+_g‘𝐴)
100	84, 99	ressplusg 17474	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
101	3, 100	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
102	98, 101	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘(𝐴 ↾_s 𝑈)))
103	102	oveqdr 7455	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+_g‘𝐶)𝑦) = (𝑥(+_g‘(𝐴 ↾_s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
106		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
107	26, 106	sralvec 34270	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 21393	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
113		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 21165	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
115	114	3expb 1138	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
116	110, 115	sylan 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
117		fedgmul.b	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118	117, 1, 3	drgextvsca 34276	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
119	43, 118	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
120	84, 75	ressvsca 17527	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
121	3, 120	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
122	5, 67	ressmulr 17490	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (._r‘𝐸) = (._r‘𝐹))
123	3, 122	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = (._r‘𝐹))
124	26, 104, 4	drgextvsca 34276	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐹) = ( ·_𝑠 ‘𝐶))
125	123, 118, 124	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐶))
126	119, 121, 125	3eqtr3rd 2807	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
127	126	oveqdr 7455	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) = (𝑥( ·_𝑠 ‘(𝐴 ↾_s 𝑈))𝑦))
128		ovexd 7462	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾_s 𝑈) ∈ V)
129	87, 91, 92, 103, 116, 127, 108, 128	lindspropd 33991	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾_s 𝑈)))
130	82, 129	eleqtrd 2865	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)))
131	76, 84	lsslinds 22149	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132	131	biimpa 482	. . . . . . . . . 10 ⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
133	15, 79, 80, 130, 132	syl31anc 1400	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴))
134		eqid 2763	. . . . . . . . . . 11 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
135		eqid 2763	. . . . . . . . . . 11 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
136	74, 73, 72, 75, 134, 135	islinds5 33976	. . . . . . . . . 10 ⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
137	136	biimpa 482	. . . . . . . . 9 ⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
138	15, 39, 133, 137	syl21anc 851	. . . . . . . 8 ⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
139	138	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
140		eqid 2763	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
141		fvexd 6908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) ∈ V)
142		fedgmullem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
143	142	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵))
144	16	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145		fedgmullem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146		fvexd 6908	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
147	142, 16	xpexd 7772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
148		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150	148, 73, 135, 149	frlmelbas 22074	. . . . . . . . . . . . . . . 16 ⊢ (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴)))))
151	146, 147, 150	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴)))))
152	145, 151	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴))))
153	152	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)))
154		fvexd 6908	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155	154, 147	elmapd 8871	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156	153, 155	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157	156	ffnd 6718	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
158	157	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
160	152	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0_g‘(Scalar‘𝐴)))
161		drngring 20999	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
162	1, 161	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
163		ringmnd 20482	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164	162, 163	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
165		subrgsubg 20841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
166	9, 165	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
167		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
168	167	subg0cl 19356	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ 𝑉)
169	166, 168	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑉)
170	46, 169	sseldd 3913	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑈)
171	5, 21, 167	ress0g 18966	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐹))
172	164, 170, 23, 171	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐹))
173	54	fveq2d 6897	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐾) = (0_g‘(Scalar‘𝐶)))
174	11, 167	subrg0 20843	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0_g‘𝐸) = (0_g‘𝐾))
175	9, 174	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐾))
176	60	fveq2d 6897	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐶)))
177	173, 175, 176	3eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘(Scalar‘𝐴)))
178	172, 177	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
179	160, 178	breqtrrd 5135	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0_g‘𝐹))
180	179	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0_g‘𝐹))
181	140, 141, 143, 144, 158, 159, 180	fsuppcurry1 33369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘𝐹))
182	178	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
183	181, 182	breqtrd 5133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)))
184		eqidd 2764	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
185	156	fovcdmda 7599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186	185	anassrs 473	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	184, 186	fvmpt2d 7015	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188	187	oveq1d 7442	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
189	119	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
190	189	oveqd 7444	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
191	188, 190	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
192	191	mpteq2dva 5200	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
193	192	oveq2d 7443	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
194	1	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing)
195	9	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸))
196	2	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing)
197	10, 194, 195, 11, 196, 144	drgextgsum 34280	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
198	3	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199	104	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
200	117, 194, 198, 5, 199, 144	drgextgsum 34280	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
201	197, 200	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
202	193, 201	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
203	142	mptexd 7237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ V)
204		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘𝐵) = (0_g‘𝐵)
205	117, 5	sralvec 34270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
206	1, 104, 3, 205	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
207		lveclmod 21393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208	206, 207	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
209	208	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
210		lmodabl 21196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211	209, 210	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
212	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213	212, 3, 23	srasubrg 34269	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
214		subrgsubg 20841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215	213, 214	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵))
216	215	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217	110	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
218	61	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219	186, 218	eleqtrd 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
220	20	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
221		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
222	220, 221	sseldd 3913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
223	17, 111, 112, 113	lmodvscl 21165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
224	217, 219, 222, 223	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	125	oveqd 7444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
226	225	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
227	32	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
228	224, 226, 227	3eltr4d 2878	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) ∈ 𝑈)
229	228	fmpttd 7123	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
230	212, 23	srasca 21467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
231	5, 230	eqtrid 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
232	231	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
233		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
234		ovexd 7462	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
235	20, 33	sstrd 3922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
236	235	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237		simprr 785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
238	236, 237	sseldd 3913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
239	238	anassrs 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
240	212, 23	srabase 21464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241	240	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
242	239, 241	eleqtrd 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
243		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
244		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
245	144, 209, 232, 233, 234, 242, 204, 243, 244, 181	mptscmfsupp0 21214	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) finSupp (0_g‘𝐵))
246	204, 211, 144, 216, 229, 245	gsumsubgcl 20146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
247	231	fveq2d 6897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
248	25, 247	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
249	248	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250	246, 249	eleqtrd 2865	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251	250	fmpttd 7123	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252	251	ffund 6722	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
253		fvexd 6908	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) ∈ V)
254		fconstmpt 5716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0_g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
255	254	eqeq2i 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
256		ovex 7460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
257	256	rgenw 3083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
258		mpteqb 7021	. . . . . . . . . . . . . . . . . . . . 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 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
261	260	necon3abii 3004	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
262		df-ov 7430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263	262	eqcomi 2772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265	264	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0_g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
266	265	necon3abid 2994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
267	266	rexbidva 3187	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
268		rexnal 3117	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
269	267, 268	bitr2di 291	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
270	261, 269	bitrid 286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
271	270	rabbidva 3421	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))})
272		fveq2 6893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273	272	neeq1d 3017	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
274	273	dmrab 33147	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))}
275	271, 274	eqtr4di 2816	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
276		fvexd 6908	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) ∈ V)
277		suppvalfn 8196	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0_g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
278	157, 147, 276, 277	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
279	160	fsuppimpd 9372	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) ∈ Fin)
280	278, 279	eqeltrrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
281		dmfi 9335	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
282	280, 281	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
283	275, 282	eqeltrd 2863	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ∈ Fin)
284		nfv 1948	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
285		nfcv 2925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
286		nfmpt1 5206	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
287		nfcv 2925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0_g‘(Scalar‘𝐴))})
288	286, 287	nfne 3061	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})
289	288, 285	nfrabw 3450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}
290	285, 289	nfdif 4068	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
291	290	nfcri 2917	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
292	284, 291	nfan 1933	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
293		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
294	293	eldifad 4053	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
295	293	eldifbd 4054	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
296		oveq1 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297	296	mpteq2dv 5201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
298	297	neeq1d 3017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
299	298	elrab 3647	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
300	295, 299	sylnib 331	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
301	294, 300	mpnanrd 415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}))
302		nne 2962	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
303	301, 302	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
304	303, 254	eqtrdi 2814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
305		ovex 7460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
306	305	rgenw 3083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
307		mpteqb 7021	. . . . . . . . . . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
310	309	r19.21bi 3257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
311	310	oveq1d 7442	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖))
312	117, 1, 3	drgext0g 34275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐵))
313	117, 1, 3	drgext0gsca 34277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
314	312, 177, 313	3eqtr3d 2806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
315	314	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
316	315	oveq1d 7442	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖))
317	208	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod)
318	294, 242	syldanl 614	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
319		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
320		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
321	233, 319, 244, 320, 204	lmod0vs 21182	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
322	317, 318, 321	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
323	311, 316, 322	3eqtrd 2802	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
324	292, 323	mpteq2da 5199	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵)))
325	324	oveq2d 7443	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))))
326		ablgrp 20011	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
327		grpmnd 19163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
328	208, 210, 326, 327	4syl 20	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
329	204	gsumz 19044	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
330	328, 16, 329	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
331	330	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
332	313	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
333	325, 331, 332	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
334	333, 142	suppss2 8228	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) supp (0_g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
335		suppssfifsupp 9382	. . . . . . . . . . . . . 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 1405	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)))
337		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
338		ovexd 7462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V)
339	337, 338	fvmpt2d 7015	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
340	339	oveq1d 7442	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
341	340	mpteq2dva 5200	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
342	341	oveq2d 7443	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
343	119	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
344	43	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
345	344	oveqd 7444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
346	345	mpteq2dva 5200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))
347	118	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
348	347	oveqd 7444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
349	348	mpteq2dv 5201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
350	346, 349	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
351	350	oveq2d 7443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
352		eqidd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
353	343, 351, 352	oveq123d 7448	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
354	201	oveq1d 7442	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
355	353, 354	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
356	355	mpteq2dva 5200	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
357	356	oveq2d 7443	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
358	10, 21	sraring 21473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
359	162, 36, 358	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
360		ringcmn 20523	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
361	359, 360	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
362	162	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
363		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
364	233, 363	lbsss 21364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
365	142, 364	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
366	365, 240	sseqtrrd 3949	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
367	366	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
368		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
369	367, 368	sseldd 3913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
370	21, 67	ringcl 20489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
371	362, 238, 369, 370	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
372	37	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴))
373	371, 372	eleqtrd 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
374	373	ralrimivva 3208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
375		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗))
376	375	fmpo 8087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
377	374, 376	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378	72, 73, 75, 74, 15, 156, 377, 147	lcomf 21188	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
379	72, 73, 75, 74, 15, 156, 377, 147, 134, 135, 160	lcomfsupp 21189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) finSupp (0_g‘𝐴))
380	74, 134, 361, 142, 16, 378, 379	gsumxp 20202	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))))
381		fedgmullem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (0_g‘𝐴))
382	162	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
383	156	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
384	57, 55	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
385	384, 36	eqsstrrd 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
386	61, 385	eqsstrd 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
387	386, 37	sseqtrd 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
388	387	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389	383, 388	fssd 6735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
390		simp2 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
391		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
392	389, 390, 391	fovcdmd 7600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
393	37	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
394	392, 393	eleqtrrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
395	238	3impb 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
396	369	3impb 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
397	21, 67	ringass 20492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
398	382, 394, 395, 396, 397	syl13anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
399	398	mpoeq3dva 7504	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
400		ovexd 7462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
401		ovexd 7462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(._r‘𝐸)𝑗) ∈ V)
402		fnov 7558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
403	157, 402	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
404	375	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗)))
405	142, 16, 400, 401, 403, 404	offval22 8107	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
406	43	ofeqd 7702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘_f (._r‘𝐸) = ∘_f ( ·_𝑠 ‘𝐴))
407	406	oveqd 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷))
408	399, 405, 407	3eqtr2rd 2805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
409	408	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
410	409	oveqd 7444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖))
411		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
412		ovexd 7462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V)
413		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
414	413	ovmpt4g 7574	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
415	411, 221, 412, 414	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
416	410, 415	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
417	416	mpteq2dva 5200	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
418	417	oveq2d 7443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))))
419	162	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
420	366	sselda 3912	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
421	162	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
422	385	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
423	422, 219	sseldd 3913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
424	21, 67	ringcl 20489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
425	421, 423, 239, 424	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
426	312	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐸) = (0_g‘𝐵))
427	245, 349, 426	3brtr4d 5139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) finSupp (0_g‘𝐸))
428	21, 167, 67, 419, 144, 420, 425, 427	gsummulc1 20557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
429	418, 428	eqtrd 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
430	144	mptexd 7237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
431	15	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
432	36	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
433	10, 430, 194, 431, 432	gsumsra 33661	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))
434	144	mptexd 7237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) ∈ V)
435	10, 434, 194, 431, 432	gsumsra 33661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))))
436	435	oveq1d 7442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
437	43	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
438	346	oveq2d 7443	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))))
439	437, 438, 352	oveq123d 7448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
440	436, 439	eqtrd 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
441	429, 433, 440	3eqtr3d 2806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
442	441	mpteq2dva 5200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)))
443	442	oveq2d 7443	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))))
444	380, 381, 443	3eqtr3rd 2807	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐴))
445	10, 1, 9	drgext0g 34275	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐴))
446	444, 445, 312	3eqtr2d 2804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐵))
447	10, 1, 9, 11, 2, 142	drgextgsum 34280	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
448	117, 1, 3, 5, 104, 142	drgextgsum 34280	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
449	447, 448	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
450	357, 446, 449	3eqtr3rd 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
451	342, 450	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
452		breq1 5108	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0_g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵))))
453		nfmpt1 5206	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
454	453	nfeq2 2942	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
455		fveq1 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗))
456	455	oveq1d 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
457	456	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
458	454, 457	mpteq2da 5199	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
459	458	oveq2d 7443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
460	459	eqeq1d 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵) ↔ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)))
461	452, 460	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))))
462		eqeq1 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
463	461, 462	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‘𝐵))}))))
464	363	lbslinds 22151	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
465	464, 142	sselid 3910	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
466		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
467	233, 466, 319, 244, 204, 320	islinds5 33976	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}))))
468	467	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
469	208, 365, 465, 468	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
470		fvexd 6908	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
471		elmapg 8870	. . . . . . . . . . . . . . . 16 ⊢ (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
472	471	biimpar 483	. . . . . . . . . . . . . . 15 ⊢ ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
473	470, 142, 251, 472	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
474	463, 469, 473	rspcdva 3580	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
475	336, 451, 474	mp2and 712	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))}))
476		fconstmpt 5716	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0_g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵)))
477	475, 476	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))))
478		ovex 7460	. . . . . . . . . . . . 13 ⊢ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
479	478	rgenw 3083	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
480		mpteqb 7021	. . . . . . . . . . . 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 221	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
483	482	r19.21bi 3257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
484	312, 445, 313	3eqtr3rd 2807	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
485	484	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
486	202, 483, 485	3eqtrd 2802	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))
487	183, 486	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
488	186	fmpttd 7123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
489		fvexd 6908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
490	489, 144	elmapd 8871	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
491	488, 490	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋))
492		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
493	492	breq1d 5115	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴))))
494		nfv 1948	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
495		nfmpt1 5206	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
496	495	nfeq2 2942	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
497	494, 496	nfan 1933	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
498		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
499	498	fveq1d 6895	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
500	499	oveq1d 7442	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))
501	497, 500	mpteq2da 5199	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)))
502	501	oveq2d 7443	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))))
503	502	eqeq1d 2765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴) ↔ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
504	493, 503	anbi12d 644	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))))
505	492	eqeq1d 2765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
506	504, 505	imbi12d 347	. . . . . . . 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 3571	. . . . . . 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 50	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
509	508, 254	eqtrdi 2814	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
510	509, 308	sylib 221	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
511	510	ralrimiva 3157	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
512		eqidd 2764	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴)))
513		fvexd 6908	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
514		fvexd 6908	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
515	157, 512, 513, 514	fnmpoovd 8106	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
516	511, 515	mpbird 260	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
517		fconstmpo 7544	. 2 ⊢ ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
518	516, 517	eqtr4di 2816	1 ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2146 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 {crab 3415 Vcvv 3453 ⊆ wss 3899 ∖ cdif 4047 {csn 4587 ⟨cop 4837 class class class wbr 5105 ↦ cmpt 5188 × cxp 5652 dom cdm 5654 Fun wfun 6540 Fn wfn 6541 ⟶wf 6542 ‘cfv 6546 (class class class)co 7427 ∈ cmpo 7429 ∘_f cof 7698 supp csupp 8187 ↑_m cmap 8858 Fincfn 8984 finSupp cfsupp 9364 Basecbs 17399 ↾_s cress 17420 +_gcplusg 17440 ._rcmulr 17441 Scalarcsca 17443 ·_𝑠 cvsca 17444 0_gc0g 17622 Σ_g cgsu 17623 Mndcmnd 18935 Grpcgrp 19156 SubGrpcsubg 19342 CMndccmn 20006 Abelcabl 20007 Ringcrg 20471 SubRingcsubrg 20833 DivRingcdr 20992 LModclmod 21147 LSubSpclss 21218 LBasisclbs 21361 LVecclvec 21389 subringAlg csra 21458 freeLMod cfrlm 22064 LIndSclinds 22123

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4838 df-uni 4870 df-int 4910 df-iun 4955 df-iin 4956 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-se 5608 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-isom 6555 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-of 7700 df-om 7885 df-1st 8008 df-2nd 8009 df-supp 8188 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-2o 8488 df-er 8728 df-map 8860 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9365 df-sup 9444 df-oi 9514 df-card 10030 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-nn 12346 df-2 12415 df-3 12416 df-4 12417 df-5 12418 df-6 12419 df-7 12420 df-8 12421 df-9 12422 df-n0 12617 df-z 12704 df-dec 12825 df-uz 12976 df-fz 13650 df-fzo 13799 df-seq 14155 df-hash 14485 df-struct 17337 df-sets 17354 df-slot 17372 df-ndx 17384 df-base 17400 df-ress 17421 df-plusg 17453 df-mulr 17454 df-sca 17456 df-vsca 17457 df-ip 17458 df-tset 17459 df-ple 17460 df-ds 17462 df-hom 17464 df-cco 17465 df-0g 17624 df-gsum 17625 df-prds 17630 df-pws 17632 df-mre 17768 df-mrc 17769 df-acs 17771 df-mgm 18828 df-sgrp 18920 df-mnd 18936 df-mhm 18990 df-submnd 18991 df-grp 19159 df-minusg 19160 df-sbg 19161 df-mulg 19290 df-subg 19345 df-ghm 19440 df-cntz 19543 df-cmn 20008 df-abl 20009 df-mgp 20373 df-rng 20387 df-ur 20420 df-ring 20473 df-nzr 20775 df-subrng 20810 df-subrg 20834 df-drng 20994 df-lmod 21149 df-lss 21219 df-lsp 21259 df-lmhm 21309 df-lbs 21362 df-lvec 21390 df-sra 21460 df-rgmod 21461 df-dsmm 22050 df-frlm 22065 df-uvc 22101 df-lindf 22124 df-linds 22125

This theorem is used by: fedgmul 34316

W3C validator