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 31711

Description: Lemma for fedgmul 31712. (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 20050	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
7	6	biimpa 477	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	3, 4, 7	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
9	8	simpld 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
10		fedgmul.a	. . . . . . . . . . . 12 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11		fedgmul.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (𝐸 ↾_s 𝑉)
12	10, 11	sralvec 31675	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 20368	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2738	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2738	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 20339	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 20025	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 16949	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 20025	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 20441	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 3960	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 20025	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 20441	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 3961	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3931	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 31674	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 20030	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 31678	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
44	43	oveqdr 7303	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) = (𝑥( ·_𝑠 ‘𝐴)𝑦))
45	3	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
46	8	simprd 496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
47	46	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈)
48		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49		ressabs 16959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
50	3, 46, 49	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
51	5	oveq1i 7285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
52	50, 51, 11	3eqtr4g 2803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
53	27, 30	srasca 20447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 16949	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 20447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
59	11, 58	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	52, 53, 59	3eqtr3rd 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2842	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3922	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝐸) = (._r‘𝐸)
68	67	subrgmcl 20036	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3123	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2738	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2738	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2738	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2738	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
76		eqid 2738	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 20224	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)))
78	77	biimpar 478	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
79	15, 42, 71, 78	syl12anc 834	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴))
80	20, 32	sseqtrrd 3962	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 21040	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sselid 3919	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 3961	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾_s 𝑈) = (𝐴 ↾_s 𝑈)
85	84, 74	ressbas2 16949	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
86	83, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
87	25, 86, 31	3eqtr3rd 2787	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾_s 𝑈)))
88	84, 72	resssca 17053	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
89	3, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
90	60, 89	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾_s 𝑈)))
91	90	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾_s 𝑈))))
92	90	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘(𝐴 ↾_s 𝑈))))
93		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐸) = (+_g‘𝐸)
94	5, 93	ressplusg 17000	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐸) = (+_g‘𝐹))
95	3, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐹))
96	34, 36	sraaddg 20443	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐴))
97	27, 30	sraaddg 20443	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘𝐶))
98	95, 96, 97	3eqtr3rd 2787	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘𝐴))
99		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝐴) = (+_g‘𝐴)
100	84, 99	ressplusg 17000	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
101	3, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
102	98, 101	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘(𝐴 ↾_s 𝑈)))
103	102	oveqdr 7303	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+_g‘𝐶)𝑦) = (𝑥(+_g‘(𝐴 ↾_s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
106		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
107	26, 106	sralvec 31675	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 20368	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
113		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 20140	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·_𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
115	114	3expb 1119	. . . . . . . . . . . . 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 31678	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
119	43, 118	eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
120	84, 75	ressvsca 17054	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
121	3, 120	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
122	5, 67	ressmulr 17017	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (._r‘𝐸) = (._r‘𝐹))
123	3, 122	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = (._r‘𝐹))
124	26, 104, 4	drgextvsca 31678	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐹) = ( ·_𝑠 ‘𝐶))
125	123, 118, 124	3eqtr3d 2786	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐶))
126	119, 121, 125	3eqtr3rd 2787	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
127	126	oveqdr 7303	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) = (𝑥( ·_𝑠 ‘(𝐴 ↾_s 𝑈))𝑦))
128		ovexd 7310	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾_s 𝑈) ∈ V)
129	87, 91, 92, 103, 116, 127, 108, 128	lindspropd 31577	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾_s 𝑈)))
130	82, 129	eleqtrd 2841	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)))
131	76, 84	lsslinds 21038	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132	131	biimpa 477	. . . . . . . . . 10 ⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
133	15, 79, 80, 130, 132	syl31anc 1372	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴))
134		eqid 2738	. . . . . . . . . . 11 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
135		eqid 2738	. . . . . . . . . . 11 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
136	74, 73, 72, 75, 134, 135	islinds5 31563	. . . . . . . . . 10 ⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
137	136	biimpa 477	. . . . . . . . 9 ⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
138	15, 39, 133, 137	syl21anc 835	. . . . . . . 8 ⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
139	138	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
140		eqid 2738	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
141		fvexd 6789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) ∈ V)
142		fedgmullem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
143	142	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵))
144	16	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145		fedgmullem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146		fvexd 6789	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
147	142, 16	xpexd 7601	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
148		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150	148, 73, 135, 149	frlmelbas 20963	. . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0_g‘(Scalar‘𝐴))))
153	152	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)))
154		fvexd 6789	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155	154, 147	elmapd 8629	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156	153, 155	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157	156	ffnd 6601	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
158	157	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
160	152	simprd 496	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0_g‘(Scalar‘𝐴)))
161		drngring 19998	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
162	1, 161	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
163		ringmnd 19793	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164	162, 163	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
165		subrgsubg 20030	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
166	9, 165	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
167		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
168	167	subg0cl 18763	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ 𝑉)
169	166, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑉)
170	46, 169	sseldd 3922	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑈)
171	5, 21, 167	ress0g 18413	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐹))
172	164, 170, 23, 171	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐹))
173	54	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐾) = (0_g‘(Scalar‘𝐶)))
174	11, 167	subrg0 20031	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0_g‘𝐸) = (0_g‘𝐾))
175	9, 174	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐾))
176	60	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐶)))
177	173, 175, 176	3eqtr4d 2788	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘(Scalar‘𝐴)))
178	172, 177	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
179	160, 178	breqtrrd 5102	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0_g‘𝐹))
180	179	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0_g‘𝐹))
181	140, 141, 143, 144, 158, 159, 180	fsuppcurry1 31060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘𝐹))
182	178	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
183	181, 182	breqtrd 5100	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)))
184		eqidd 2739	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
185	156	fovrnda 7443	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186	185	anassrs 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	184, 186	fvmpt2d 6888	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188	187	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
189	119	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
190	189	oveqd 7292	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
191	188, 190	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
192	191	mpteq2dva 5174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
193	192	oveq2d 7291	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
194	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing)
195	9	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸))
196	2	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing)
197	10, 194, 195, 11, 196, 144	drgextgsum 31682	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
198	3	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199	104	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
200	117, 194, 198, 5, 199, 144	drgextgsum 31682	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
201	197, 200	eqtr3d 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
202	193, 201	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
203	142	mptexd 7100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ V)
204		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘𝐵) = (0_g‘𝐵)
205	117, 5	sralvec 31675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
206	1, 104, 3, 205	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
207		lveclmod 20368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208	206, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
209	208	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
210		lmodabl 20170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
212	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213	212, 3, 23	srasubrg 31674	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
214		subrgsubg 20030	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵))
216	215	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217	110	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
218	61	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219	186, 218	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
220	20	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
221		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
222	220, 221	sseldd 3922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
223	17, 111, 112, 113	lmodvscl 20140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
224	217, 219, 222, 223	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	125	oveqd 7292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
226	225	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
227	32	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
228	224, 226, 227	3eltr4d 2854	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) ∈ 𝑈)
229	228	fmpttd 6989	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
230	212, 23	srasca 20447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
231	5, 230	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
232	231	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
233		eqid 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
234		ovexd 7310	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
235	20, 33	sstrd 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
236	235	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237		simprr 770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
238	236, 237	sseldd 3922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
239	238	anassrs 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
240	212, 23	srabase 20441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241	240	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
242	239, 241	eleqtrd 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
243		eqid 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
244		eqid 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
245	144, 209, 232, 233, 234, 242, 204, 243, 244, 181	mptscmfsupp0 20188	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) finSupp (0_g‘𝐵))
246	204, 211, 144, 216, 229, 245	gsumsubgcl 19521	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
247	231	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
248	25, 247	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
249	248	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250	246, 249	eleqtrd 2841	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251	250	fmpttd 6989	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252	251	ffund 6604	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
253		fvexd 6789	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) ∈ V)
254		fconstmpt 5649	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0_g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
255	254	eqeq2i 2751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
256		ovex 7308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
257	256	rgenw 3076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
258		mpteqb 6894	. . . . . . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
261	260	necon3abii 2990	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
262		df-ov 7278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263	262	eqcomi 2747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265	264	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0_g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
266	265	necon3abid 2980	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
267	266	rexbidva 3225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
268		rexnal 3169	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
269	267, 268	bitr2di 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
270	261, 269	syl5bb 283	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
271	270	rabbidva 3413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))})
272		fveq2 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273	272	neeq1d 3003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
274	273	dmrab 30844	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))}
275	271, 274	eqtr4di 2796	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
276		fvexd 6789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) ∈ V)
277		suppvalfn 7985	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0_g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
278	157, 147, 276, 277	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
279	160	fsuppimpd 9135	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) ∈ Fin)
280	278, 279	eqeltrrd 2840	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
281		dmfi 9097	. . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ∈ Fin)
284		nfv 1917	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
285		nfcv 2907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
286		nfmpt1 5182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
287		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0_g‘(Scalar‘𝐴))})
288	286, 287	nfne 3045	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})
289	288, 285	nfrabw 3318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}
290	285, 289	nfdif 4060	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
291	290	nfcri 2894	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
292	284, 291	nfan 1902	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
293		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
294	293	eldifad 3899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
295	293	eldifbd 3900	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
296		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297	296	mpteq2dv 5176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
298	297	neeq1d 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
299	298	elrab 3624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
300	295, 299	sylnib 328	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
301	294, 300	mpnanrd 410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}))
302		nne 2947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
303	301, 302	sylib 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
304	303, 254	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
305		ovex 7308	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
306	305	rgenw 3076	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
307		mpteqb 6894	. . . . . . . . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
310	309	r19.21bi 3134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
311	310	oveq1d 7290	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖))
312	117, 1, 3	drgext0g 31677	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐵))
313	117, 1, 3	drgext0gsca 31679	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
314	312, 177, 313	3eqtr3d 2786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
315	314	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
316	315	oveq1d 7290	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐵))( ·_𝑠 ‘𝐵)𝑖))
317	208	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod)
318	294, 242	syldanl 602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
319		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
320		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
321	233, 319, 244, 320, 204	lmod0vs 20156	. . . . . . . . . . . . . . . . . . . 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 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
324	292, 323	mpteq2da 5172	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵)))
325	324	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))))
326	208, 210	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ Abel)
327		ablgrp 19391	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
328		grpmnd 18584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
329	326, 327, 328	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
330	204	gsumz 18474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
331	329, 16, 330	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
332	331	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))) = (0_g‘𝐵))
333	313	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
334	325, 332, 333	3eqtrd 2782	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
335	334, 142	suppss2 8016	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) supp (0_g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
336		suppssfifsupp 9143	. . . . . . . . . . . . . 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‘𝐵)))
337	203, 252, 253, 283, 335, 336	syl32anc 1377	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)))
338		eqidd 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
339		ovexd 7310	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V)
340	338, 339	fvmpt2d 6888	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
341	340	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
342	341	mpteq2dva 5174	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
343	342	oveq2d 7291	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
344	119	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
345	43	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
346	345	oveqd 7292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
347	346	mpteq2dva 5174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))
348	118	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
349	348	oveqd 7292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
350	349	mpteq2dv 5176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
351	347, 350	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
352	351	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
353		eqidd 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
354	344, 352, 353	oveq123d 7296	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
355	201	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
356	354, 355	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
357	356	mpteq2dva 5174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
358	357	oveq2d 7291	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
359	10, 21	sraring 31672	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
360	162, 36, 359	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
361		ringcmn 19820	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
362	360, 361	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
363	162	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
364		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
365	233, 364	lbsss 20339	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
366	142, 365	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
367	366, 240	sseqtrrd 3962	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
368	367	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
369		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
370	368, 369	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
371	21, 67	ringcl 19800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
372	363, 238, 370, 371	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐸))
373	37	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴))
374	372, 373	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
375	374	ralrimivva 3123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
376		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗))
377	376	fmpo 7908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378	375, 377	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
379	72, 73, 75, 74, 15, 156, 378, 147	lcomf 20162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
380	72, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160	lcomfsupp 20163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) finSupp (0_g‘𝐴))
381	74, 134, 362, 142, 16, 379, 380	gsumxp 19577	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))))
382		fedgmullem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)) = (0_g‘𝐴))
383	162	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
384	156	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
385	57, 55	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
386	385, 36	eqsstrrd 3960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
387	61, 386	eqsstrd 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
388	387, 37	sseqtrd 3961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389	388	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390	384, 389	fssd 6618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
391		simp2 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
392		simp3 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
393	390, 391, 392	fovrnd 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
394	37	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
395	393, 394	eleqtrrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
396	238	3impb 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
397	370	3impb 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
398	21, 67	ringass 19803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
399	383, 395, 396, 397, 398	syl13anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗)))
400	399	mpoeq3dva 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
401		ovexd 7310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
402		ovexd 7310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(._r‘𝐸)𝑗) ∈ V)
403		fnov 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
404	157, 403	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
405	376	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗)))
406	142, 16, 401, 402, 404, 405	offval22 7928	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
407	43	ofeqd 7535	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘_f (._r‘𝐸) = ∘_f ( ·_𝑠 ‘𝐴))
408	407	oveqd 7292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷))
409	400, 406, 408	3eqtr2rd 2785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
410	409	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
411	410	oveqd 7292	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖))
412		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
413		ovexd 7310	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V)
414		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
415	414	ovmpt4g 7420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
416	412, 221, 413, 415	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
417	411, 416	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
418	417	mpteq2dva 5174	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
419	418	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))))
420	162	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
421	367	sselda 3921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
422	162	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
423	386	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
424	423, 219	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
425	21, 67	ringcl 19800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
426	422, 424, 239, 425	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) ∈ (Base‘𝐸))
427	312	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐸) = (0_g‘𝐵))
428	245, 350, 427	3brtr4d 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) finSupp (0_g‘𝐸))
429	21, 167, 93, 67, 420, 144, 421, 426, 428	gsummulc1 19845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
430	419, 429	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
431	144	mptexd 7100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
432	15	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
433	36	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
434	10, 431, 194, 432, 433	gsumsra 31307	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))
435	144	mptexd 7100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) ∈ V)
436	10, 435, 194, 432, 433	gsumsra 31307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))))
437	436	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
438	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
439	347	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))))
440	438, 439, 353	oveq123d 7296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
441	437, 440	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
442	430, 434, 441	3eqtr3d 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
443	442	mpteq2dva 5174	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)))
444	443	oveq2d 7291	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))))
445	381, 382, 444	3eqtr3rd 2787	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐴))
446	10, 1, 9	drgext0g 31677	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐴))
447	445, 446, 312	3eqtr2d 2784	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐵))
448	10, 1, 9, 11, 2, 142	drgextgsum 31682	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
449	117, 1, 3, 5, 104, 142	drgextgsum 31682	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
450	448, 449	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
451	358, 447, 450	3eqtr3rd 2787	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
452	343, 451	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
453		breq1 5077	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0_g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵))))
454		nfmpt1 5182	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
455	454	nfeq2 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
456		fveq1 6773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗))
457	456	oveq1d 7290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
458	457	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
459	455, 458	mpteq2da 5172	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
460	459	oveq2d 7291	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
461	460	eqeq1d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵) ↔ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)))
462	453, 461	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))))
463		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
464	462, 463	imbi12d 345	. . . . . . . . . . . . . 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‘𝐵))}))))
465	364	lbslinds 21040	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
466	465, 142	sselid 3919	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
467		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
468	233, 467, 319, 244, 204, 320	islinds5 31563	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))}))))
469	468	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
470	208, 366, 466, 469	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌)((𝑏 finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → 𝑏 = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
471		fvexd 6789	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
472		elmapg 8628	. . . . . . . . . . . . . . . 16 ⊢ (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
473	472	biimpar 478	. . . . . . . . . . . . . . 15 ⊢ ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
474	471, 142, 251, 473	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑_m 𝑌))
475	464, 470, 474	rspcdva 3562	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵)) ∧ (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))})))
476	337, 452, 475	mp2and 696	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0_g‘(Scalar‘𝐵))}))
477		fconstmpt 5649	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0_g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵)))
478	476, 477	eqtrdi 2794	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))))
479		ovex 7308	. . . . . . . . . . . . 13 ⊢ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
480	479	rgenw 3076	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
481		mpteqb 6894	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵))))
482	480, 481	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
483	478, 482	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
484	483	r19.21bi 3134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
485	312, 446, 313	3eqtr3rd 2787	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
486	485	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
487	202, 484, 486	3eqtrd 2782	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))
488	183, 487	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
489	186	fmpttd 6989	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
490		fvexd 6789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
491	490, 144	elmapd 8629	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
492	489, 491	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋))
493		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
494	493	breq1d 5084	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴))))
495		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
496		nfmpt1 5182	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
497	496	nfeq2 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
498	495, 497	nfan 1902	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
499		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
500	499	fveq1d 6776	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
501	500	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))
502	498, 501	mpteq2da 5172	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)))
503	502	oveq2d 7291	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))))
504	503	eqeq1d 2740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴) ↔ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
505	494, 504	anbi12d 631	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))))
506	493	eqeq1d 2740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))})))
507	505, 506	imbi12d 345	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
508	492, 507	rspcdv 3553	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋)((𝑤 finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → 𝑤 = (𝑋 × {(0_g‘(Scalar‘𝐴))})) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))))
509	139, 488, 508	mp2d 49	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
510	509, 254	eqtrdi 2794	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
511	510, 308	sylib 217	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
512	511	ralrimiva 3103	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
513		eqidd 2739	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴)))
514		fvexd 6789	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
515		fvexd 6789	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
516	157, 513, 514, 515	fnmpoovd 7927	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
517	512, 516	mpbird 256	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
518		fconstmpo 7391	. 2 ⊢ ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
519	517, 518	eqtr4di 2796	1 ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3432 ∖ cdif 3884 ⊆ wss 3887 {csn 4561 ⟨cop 4567 class class class wbr 5074 ↦ cmpt 5157 × cxp 5587 dom cdm 5589 Fun wfun 6427 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ∈ cmpo 7277 ∘_f cof 7531 supp csupp 7977 ↑_m cmap 8615 Fincfn 8733 finSupp cfsupp 9128 Basecbs 16912 ↾_s cress 16941 +_gcplusg 16962 ._rcmulr 16963 Scalarcsca 16965 ·_𝑠 cvsca 16966 0_gc0g 17150 Σ_g cgsu 17151 Mndcmnd 18385 Grpcgrp 18577 SubGrpcsubg 18749 CMndccmn 19386 Abelcabl 19387 Ringcrg 19783 DivRingcdr 19991 SubRingcsubrg 20020 LModclmod 20123 LSubSpclss 20193 LBasisclbs 20336 LVecclvec 20364 subringAlg csra 20430 freeLMod cfrlm 20953 LIndSclinds 21012

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-map 8617 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-sup 9201 df-oi 9269 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-fz 13240 df-fzo 13383 df-seq 13722 df-hash 14045 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-hom 16986 df-cco 16987 df-0g 17152 df-gsum 17153 df-prds 17158 df-pws 17160 df-mre 17295 df-mrc 17296 df-acs 17298 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-mhm 18430 df-submnd 18431 df-grp 18580 df-minusg 18581 df-sbg 18582 df-mulg 18701 df-subg 18752 df-ghm 18832 df-cntz 18923 df-cmn 19388 df-abl 19389 df-mgp 19721 df-ur 19738 df-ring 19785 df-drng 19993 df-subrg 20022 df-lmod 20125 df-lss 20194 df-lsp 20234 df-lmhm 20284 df-lbs 20337 df-lvec 20365 df-sra 20434 df-rgmod 20435 df-nzr 20529 df-dsmm 20939 df-frlm 20954 df-uvc 20990 df-lindf 21013 df-linds 21014

This theorem is referenced by: fedgmul 31712

W3C validator