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 34086

Description: Lemma for fedgmul 34087. (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 20749	. . . . . . . . . . . . . 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 34041	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 21279	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2765	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2765	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 21250	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 20723	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 17322	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 20723	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 21350	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 3973	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 20723	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 21350	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 3974	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3948	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 34040	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 20728	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 34047	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
44	43	oveqdr 7447	. . . . . . . . . . . . 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 17332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
50	3, 46, 49	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾_s 𝑈) ↾_s 𝑉) = (𝐸 ↾_s 𝑉))
51	5	oveq1i 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾_s 𝑉) = ((𝐸 ↾_s 𝑈) ↾_s 𝑉)
52	50, 51, 11	3eqtr4g 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = 𝐾)
53	27, 30	srasca 21353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2802	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 17322	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 21353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑉) = (Scalar‘𝐴))
59	11, 58	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	52, 53, 59	3eqtr3rd 2809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2810	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2868	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3939	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝐸) = (._r‘𝐸)
68	67	subrgmcl 20735	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(._r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2866	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3210	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·_𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2765	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2765	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2765	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2765	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐴)
76		eqid 2765	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 21135	. . . . . . . . . . . 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 3975	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 22035	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sselid 3936	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 3974	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾_s 𝑈) = (𝐴 ↾_s 𝑈)
85	84, 74	ressbas2 17322	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
86	83, 85	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾_s 𝑈)))
87	25, 86, 31	3eqtr3rd 2809	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾_s 𝑈)))
88	84, 72	resssca 17420	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
89	3, 88	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾_s 𝑈)))
90	60, 89	eqtr3d 2802	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾_s 𝑈)))
91	90	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾_s 𝑈))))
92	90	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘(Scalar‘𝐶)) = (0_g‘(Scalar‘(𝐴 ↾_s 𝑈))))
93		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐸) = (+_g‘𝐸)
94	5, 93	ressplusg 17368	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐸) = (+_g‘𝐹))
95	3, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐹))
96	34, 36	sraaddg 21351	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐸) = (+_g‘𝐴))
97	27, 30	sraaddg 21351	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+_g‘𝐹) = (+_g‘𝐶))
98	95, 96, 97	3eqtr3rd 2809	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘𝐴))
99		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝐴) = (+_g‘𝐴)
100	84, 99	ressplusg 17368	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
101	3, 100	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+_g‘𝐴) = (+_g‘(𝐴 ↾_s 𝑈)))
102	98, 101	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+_g‘𝐶) = (+_g‘(𝐴 ↾_s 𝑈)))
103	102	oveqdr 7447	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+_g‘𝐶)𝑦) = (𝑥(+_g‘(𝐴 ↾_s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾_s 𝑉) ∈ DivRing)
106		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾_s 𝑉) = (𝐹 ↾_s 𝑉)
107	26, 106	sralvec 34041	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾_s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 21279	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘𝐶)
113		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 21051	. . . . . . . . . . . . . 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 34047	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
119	43, 118	eqtr3d 2802	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
120	84, 75	ressvsca 17421	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
121	3, 120	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
122	5, 67	ressmulr 17384	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (._r‘𝐸) = (._r‘𝐹))
123	3, 122	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐸) = (._r‘𝐹))
124	26, 104, 4	drgextvsca 34047	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (._r‘𝐹) = ( ·_𝑠 ‘𝐶))
125	123, 118, 124	3eqtr3d 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐶))
126	119, 121, 125	3eqtr3rd 2809	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·_𝑠 ‘𝐶) = ( ·_𝑠 ‘(𝐴 ↾_s 𝑈)))
127	126	oveqdr 7447	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·_𝑠 ‘𝐶)𝑦) = (𝑥( ·_𝑠 ‘(𝐴 ↾_s 𝑈))𝑦))
128		ovexd 7454	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾_s 𝑈) ∈ V)
129	87, 91, 92, 103, 116, 127, 108, 128	lindspropd 33762	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾_s 𝑈)))
130	82, 129	eleqtrd 2867	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾_s 𝑈)))
131	76, 84	lsslinds 22033	. . . . . . . . . . 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 2765	. . . . . . . . . . 11 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
135		eqid 2765	. . . . . . . . . . 11 ⊢ (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴))
136	74, 73, 72, 75, 134, 135	islinds5 33748	. . . . . . . . . 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 2765	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
141		fvexd 6900	. . . . . . . . . 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 6900	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
147	142, 16	xpexd 7756	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
148		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150	148, 73, 135, 149	frlmelbas 21958	. . . . . . . . . . . . . . . 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 6900	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155	154, 147	elmapd 8843	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑_m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156	153, 155	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157	156	ffnd 6710	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
158	157	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
160	152	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0_g‘(Scalar‘𝐴)))
161		drngring 20886	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
162	1, 161	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
163		ringmnd 20371	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164	162, 163	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
165		subrgsubg 20728	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
166	9, 165	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
167		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
168	167	subg0cl 19246	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0_g‘𝐸) ∈ 𝑉)
169	166, 168	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑉)
170	46, 169	sseldd 3939	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) ∈ 𝑈)
171	5, 21, 167	ress0g 18857	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0_g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0_g‘𝐸) = (0_g‘𝐹))
172	164, 170, 23, 171	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐹))
173	54	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐾) = (0_g‘(Scalar‘𝐶)))
174	11, 167	subrg0 20730	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0_g‘𝐸) = (0_g‘𝐾))
175	9, 174	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐾))
176	60	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐶)))
177	173, 175, 176	3eqtr4d 2810	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘(Scalar‘𝐴)))
178	172, 177	eqtr3d 2802	. . . . . . . . . . . 12 ⊢ (𝜑 → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
179	160, 178	breqtrrd 5141	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0_g‘𝐹))
180	179	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0_g‘𝐹))
181	140, 141, 143, 144, 158, 159, 180	fsuppcurry1 33141	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘𝐹))
182	178	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘𝐹) = (0_g‘(Scalar‘𝐴)))
183	181, 182	breqtrd 5139	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)))
184		eqidd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
185	156	fovcdmda 7591	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186	185	anassrs 473	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	184, 186	fvmpt2d 7007	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188	187	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
189	119	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
190	189	oveqd 7436	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
191	188, 190	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
192	191	mpteq2dva 5206	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
193	192	oveq2d 7435	. . . . . . . . . 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 34051	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
198	3	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199	104	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
200	117, 194, 198, 5, 199, 144	drgextgsum 34051	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
201	197, 200	eqtr3d 2802	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
202	193, 201	eqtrd 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
203	142	mptexd 7229	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∈ V)
204		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘𝐵) = (0_g‘𝐵)
205	117, 5	sralvec 34041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
206	1, 104, 3, 205	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
207		lveclmod 21279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208	206, 207	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
209	208	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
210		lmodabl 21082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211	209, 210	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
212	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213	212, 3, 23	srasubrg 34040	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
214		subrgsubg 20728	. . . . . . . . . . . . . . . . . . . 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 2867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
220	20	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
221		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
222	220, 221	sseldd 3939	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
223	17, 111, 112, 113	lmodvscl 21051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
224	217, 219, 222, 223	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	125	oveqd 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
226	225	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐶)𝑖))
227	32	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
228	224, 226, 227	3eltr4d 2880	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) ∈ 𝑈)
229	228	fmpttd 7114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
230	212, 23	srasca 21353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾_s 𝑈) = (Scalar‘𝐵))
231	5, 230	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
232	231	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
233		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
234		ovexd 7454	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
235	20, 33	sstrd 3948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
236	235	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237		simprr 785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
238	236, 237	sseldd 3939	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
239	238	anassrs 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
240	212, 23	srabase 21350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241	240	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
242	239, 241	eleqtrd 2867	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
243		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
244		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·_𝑠 ‘𝐵) = ( ·_𝑠 ‘𝐵)
245	144, 209, 232, 233, 234, 242, 204, 243, 244, 181	mptscmfsupp0 21100	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) finSupp (0_g‘𝐵))
246	204, 211, 144, 216, 229, 245	gsumsubgcl 20036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
247	231	fveq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
248	25, 247	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
249	248	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250	246, 249	eleqtrd 2867	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251	250	fmpttd 7114	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252	251	ffund 6714	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
253		fvexd 6900	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) ∈ V)
254		fconstmpt 5725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0_g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
255	254	eqeq2i 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
256		ovex 7452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
257	256	rgenw 3085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
258		mpteqb 7013	. . . . . . . . . . . . . . . . . . . . 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 3006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
262		df-ov 7422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263	262	eqcomi 2774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265	264	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0_g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
266	265	necon3abid 2996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
267	266	rexbidva 3189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
268		rexnal 3119	. . . . . . . . . . . . . . . . . . 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 3424	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))})
272		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273	272	neeq1d 3019	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))))
274	273	dmrab 32916	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0_g‘(Scalar‘𝐴))}
275	271, 274	eqtr4di 2818	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))})
276		fvexd 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) ∈ V)
277		suppvalfn 8170	. . . . . . . . . . . . . . . . . 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 9336	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0_g‘(Scalar‘𝐴))) ∈ Fin)
280	278, 279	eqeltrrd 2866	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0_g‘(Scalar‘𝐴))} ∈ Fin)
281		dmfi 9299	. . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})} ∈ Fin)
284		nfv 1947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
285		nfcv 2927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
286		nfmpt1 5212	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
287		nfcv 2927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0_g‘(Scalar‘𝐴))})
288	286, 287	nfne 3063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})
289	288, 285	nfrabw 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}
290	285, 289	nfdif 4084	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
291	290	nfcri 2919	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
292	284, 291	nfan 1932	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
293		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})}))
294	293	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
295	293	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
296		oveq1 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297	296	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
298	297	neeq1d 3019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})))
299	298	elrab 3652	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
303	301, 302	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0_g‘(Scalar‘𝐴))}))
304	303, 254	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
305		ovex 7452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
306	305	rgenw 3085	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
307		mpteqb 7013	. . . . . . . . . . . . . . . . . . . . . . 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 3259	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
311	310	oveq1d 7434	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = ((0_g‘(Scalar‘𝐴))( ·_𝑠 ‘𝐵)𝑖))
312	117, 1, 3	drgext0g 34046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐵))
313	117, 1, 3	drgext0gsca 34048	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0_g‘𝐵) = (0_g‘(Scalar‘𝐵)))
314	312, 177, 313	3eqtr3d 2808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
315	314	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐵)))
316	315	oveq1d 7434	. . . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
320		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0_g‘(Scalar‘𝐵)) = (0_g‘(Scalar‘𝐵))
321	233, 319, 244, 320, 204	lmod0vs 21068	. . . . . . . . . . . . . . . . . . . 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 2804	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖) = (0_g‘𝐵))
324	292, 323	mpteq2da 5205	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵)))
325	324	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ (0_g‘𝐵))))
326		ablgrp 19901	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
327		grpmnd 19053	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
328	208, 210, 326, 327	4syl 20	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
329	204	gsumz 18934	. . . . . . . . . . . . . . . . . 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 2804	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
334	333, 142	suppss2 8202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) supp (0_g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0_g‘(Scalar‘𝐴))})})
335		suppssfifsupp 9347	. . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))))
338		ovexd 7454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V)
339	337, 338	fvmpt2d 7007	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
340	339	oveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
341	340	mpteq2dva 5206	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
342	341	oveq2d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
343	119	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·_𝑠 ‘𝐴) = ( ·_𝑠 ‘𝐵))
344	43	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
345	344	oveqd 7436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))
346	345	mpteq2dva 5206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))
347	118	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐵))
348	347	oveqd 7436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(._r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))
349	348	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
350	346, 349	eqtr3d 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))
351	350	oveq2d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
352		eqidd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
353	343, 351, 352	oveq123d 7440	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
354	201	oveq1d 7434	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
355	353, 354	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗) = ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))
356	355	mpteq2dva 5206	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗)))
357	356	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
358	10, 21	sraring 21359	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
359	162, 36, 358	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
360		ringcmn 20412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
361	359, 360	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
362	162	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
363		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
364	233, 363	lbsss 21250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
365	142, 364	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
366	365, 240	sseqtrrd 3975	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
367	366	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
368		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
369	367, 368	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
370	21, 67	ringcl 20378	. . . . . . . . . . . . . . . . . . . . . . 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 2867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
374	373	ralrimivva 3210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴))
375		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗))
376	375	fmpo 8071	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(._r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
377	374, 376	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378	72, 73, 75, 74, 15, 156, 377, 147	lcomf 21074	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
379	72, 73, 75, 74, 15, 156, 377, 147, 134, 135, 160	lcomfsupp 21075	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) finSupp (0_g‘𝐴))
380	74, 134, 361, 142, 16, 378, 379	gsumxp 20092	. . . . . . . . . . . . . . . . 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 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
385	384, 36	eqsstrrd 3973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
386	61, 385	eqsstrd 3972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
387	386, 37	sseqtrd 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
388	387	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389	383, 388	fssd 6727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
390		simp2 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
391		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
392	389, 390, 391	fovcdmd 7592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
393	37	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
394	392, 393	eleqtrrd 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
395	238	3impb 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
396	369	3impb 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
397	21, 67	ringass 20381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
400		ovexd 7454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
401		ovexd 7454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(._r‘𝐸)𝑗) ∈ V)
402		fnov 7550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
403	157, 402	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
404	375	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(._r‘𝐸)𝑗)))
405	142, 16, 400, 401, 403, 404	offval22 8089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)(𝑖(._r‘𝐸)𝑗))))
406	43	ofeqd 7686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘_f (._r‘𝐸) = ∘_f ( ·_𝑠 ‘𝐴))
407	406	oveqd 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘_f (._r‘𝐸)𝐷) = (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷))
408	399, 405, 407	3eqtr2rd 2807	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
409	408	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
410	409	oveqd 7436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖))
411		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
412		ovexd 7454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V)
413		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
414	413	ovmpt4g 7566	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
415	411, 221, 412, 414	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
416	410, 415	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))
417	416	mpteq2dva 5206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗)))
418	417	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))))
419	162	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
420	366	sselda 3938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
421	162	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
422	385	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
423	422, 219	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
424	21, 67	ringcl 20378	. . . . . . . . . . . . . . . . . . . . . . 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 5145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) finSupp (0_g‘𝐸))
428	21, 167, 67, 419, 144, 420, 425, 427	gsummulc1 20445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(._r‘𝐸)𝑖)(._r‘𝐸)𝑗))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
429	418, 428	eqtrd 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
430	144	mptexd 7229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
431	15	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
432	36	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
433	10, 430, 194, 431, 432	gsumsra 33433	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))
434	144	mptexd 7229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)) ∈ V)
435	10, 434, 194, 431, 432	gsumsra 33433	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))))
436	435	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗))
437	43	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (._r‘𝐸) = ( ·_𝑠 ‘𝐴))
438	346	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖))))
439	437, 438, 352	oveq123d 7440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
440	436, 439	eqtrd 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(._r‘𝐸)𝑖)))(._r‘𝐸)𝑗) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
441	429, 433, 440	3eqtr3d 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))
442	441	mpteq2dva 5206	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗)))
443	442	oveq2d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘_f ( ·_𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))))
444	380, 381, 443	3eqtr3rd 2809	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐴))
445	10, 1, 9	drgext0g 34046	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0_g‘𝐸) = (0_g‘𝐴))
446	444, 445, 312	3eqtr2d 2806	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐴)𝑖)))( ·_𝑠 ‘𝐴)𝑗))) = (0_g‘𝐵))
447	10, 1, 9, 11, 2, 142	drgextgsum 34051	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
448	117, 1, 3, 5, 104, 142	drgextgsum 34051	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
449	447, 448	eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))))
450	357, 446, 449	3eqtr3rd 2809	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
451	342, 450	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (0_g‘𝐵))
452		breq1 5114	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0_g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) finSupp (0_g‘(Scalar‘𝐵))))
453		nfmpt1 5212	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
454	453	nfeq2 2944	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))
455		fveq1 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗))
456	455	oveq1d 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
457	456	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))
458	454, 457	mpteq2da 5205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗)))
459	458	oveq2d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) → (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·_𝑠 ‘𝐵)𝑗))) = (𝐵 Σ_g (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))))‘𝑗)( ·_𝑠 ‘𝐵)𝑗))))
460	459	eqeq1d 2767	. . . . . . . . . . . . . . . 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 2769	. . . . . . . . . . . . . . 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 22035	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
465	464, 142	sselid 3936	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
466		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
467	233, 466, 319, 244, 204, 320	islinds5 33748	. . . . . . . . . . . . . . . 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 6900	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
471		elmapg 8842	. . . . . . . . . . . . . . . 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 3584	. . . . . . . . . . . . 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 5725	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0_g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵)))
477	475, 476	eqtrdi 2816	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0_g‘(Scalar‘𝐵))))
478		ovex 7452	. . . . . . . . . . . . 13 ⊢ (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
479	478	rgenw 3085	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) ∈ V
480		mpteqb 7013	. . . . . . . . . . . 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 3259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·_𝑠 ‘𝐵)𝑖))) = (0_g‘(Scalar‘𝐵)))
484	312, 445, 313	3eqtr3rd 2809	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
485	484	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0_g‘(Scalar‘𝐵)) = (0_g‘𝐴))
486	202, 483, 485	3eqtrd 2804	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴))
487	183, 486	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴)) ∧ (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (0_g‘𝐴)))
488	186	fmpttd 7114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
489		fvexd 6900	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
490	489, 144	elmapd 8843	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
491	488, 490	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑_m 𝑋))
492		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
493	492	breq1d 5121	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0_g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0_g‘(Scalar‘𝐴))))
494		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
495		nfmpt1 5212	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
496	495	nfeq2 2944	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
497	494, 496	nfan 1932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
498		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
499	498	fveq1d 6887	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
500	499	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))
501	497, 500	mpteq2da 5205	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖)))
502	501	oveq2d 7435	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·_𝑠 ‘𝐴)𝑖))) = (𝐴 Σ_g (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·_𝑠 ‘𝐴)𝑖))))
503	502	eqeq1d 2767	. . . . . . . . . 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 2767	. . . . . . . . 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 3575	. . . . . . 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 2816	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
510	509, 308	sylib 221	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
511	510	ralrimiva 3159	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴)))
512		eqidd 2766	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0_g‘(Scalar‘𝐴)) = (0_g‘(Scalar‘𝐴)))
513		fvexd 6900	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
514		fvexd 6900	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0_g‘(Scalar‘𝐴)) ∈ V)
515	157, 512, 513, 514	fnmpoovd 8088	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0_g‘(Scalar‘𝐴))))
516	511, 515	mpbird 260	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴))))
517		fconstmpo 7536	. 2 ⊢ ((𝑌 × 𝑋) × {(0_g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0_g‘(Scalar‘𝐴)))
518	516, 517	eqtr4di 2818	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 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 {crab 3418 Vcvv 3457 ∖ cdif 3903 ⊆ wss 3906 {csn 4591 ⟨cop 4597 class class class wbr 5111 ↦ cmpt 5194 × cxp 5661 dom cdm 5663 Fun wfun 6534 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ∈ cmpo 7421 ∘_f cof 7682 supp csupp 8162 ↑_m cmap 8830 Fincfn 8949 finSupp cfsupp 9328 Basecbs 17293 ↾_s cress 17314 +_gcplusg 17334 ._rcmulr 17335 Scalarcsca 17337 ·_𝑠 cvsca 17338 0_gc0g 17516 Σ_g cgsu 17517 Mndcmnd 18826 Grpcgrp 19046 SubGrpcsubg 19232 CMndccmn 19896 Abelcabl 19897 Ringcrg 20361 SubRingcsubrg 20720 DivRingcdr 20879 LModclmod 21033 LSubSpclss 21104 LBasisclbs 21247 LVecclvec 21275 subringAlg csra 21344 freeLMod cfrlm 21948 LIndSclinds 22007

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-sup 9409 df-oi 9479 df-card 9941 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12522 df-z 12609 df-dec 12730 df-uz 12881 df-fz 13554 df-fzo 13702 df-seq 14058 df-hash 14387 df-struct 17231 df-sets 17248 df-slot 17266 df-ndx 17278 df-base 17294 df-ress 17315 df-plusg 17347 df-mulr 17348 df-sca 17350 df-vsca 17351 df-ip 17352 df-tset 17353 df-ple 17354 df-ds 17356 df-hom 17358 df-cco 17359 df-0g 17518 df-gsum 17519 df-prds 17524 df-pws 17526 df-mre 17662 df-mrc 17663 df-acs 17665 df-mgm 18722 df-sgrp 18811 df-mnd 18827 df-mhm 18880 df-submnd 18881 df-grp 19049 df-minusg 19050 df-sbg 19051 df-mulg 19180 df-subg 19235 df-ghm 19330 df-cntz 19433 df-cmn 19898 df-abl 19899 df-mgp 20263 df-rng 20277 df-ur 20310 df-ring 20363 df-nzr 20662 df-subrng 20697 df-subrg 20721 df-drng 20881 df-lmod 21035 df-lss 21105 df-lsp 21145 df-lmhm 21195 df-lbs 21248 df-lvec 21276 df-sra 21346 df-rgmod 21347 df-dsmm 21934 df-frlm 21949 df-uvc 21985 df-lindf 22008 df-linds 22009

This theorem is used by: fedgmul 34087

W3C validator