Theorem fedgmullem2 32774

Description: Lemma for fedgmul 32775. (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 ( ·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴))

Assertion

Ref	Expression
fedgmullem2	⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0g‘(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 20349	. . . . . . . . . . . . . 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 32731	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 20722	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2732	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2732	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 20693	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 20324	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 17184	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 20324	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 20798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 4021	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 20324	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 20798	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 4022	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3992	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 32730	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 20329	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 32736	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
44	43	oveqdr 7439	. . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49		ressabs 17196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
50	3, 46, 49	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
51	5	oveq1i 7421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉)
52	50, 51, 11	3eqtr4g 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾)
53	27, 30	srasca 20804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 17184	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 20804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
59	11, 58	eqtrid 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	52, 53, 59	3eqtr3rd 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2782	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (.r‘𝐸) = (.r‘𝐸)
68	67	subrgmcl 20335	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2834	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3200	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2732	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2732	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2732	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2732	. . . . . . . . . . . . 13 ⊢ ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐴)
76		eqid 2732	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 20578	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)))
78	77	biimpar 478	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
79	15, 42, 71, 78	syl12anc 835	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴))
80	20, 32	sseqtrrd 4023	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 21394	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sselid 3980	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 4022	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾s 𝑈) = (𝐴 ↾s 𝑈)
85	84, 74	ressbas2 17184	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾s 𝑈)))
86	83, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾s 𝑈)))
87	25, 86, 31	3eqtr3rd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾s 𝑈)))
88	84, 72	resssca 17290	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈)))
89	3, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈)))
90	60, 89	eqtr3d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾s 𝑈)))
91	90	fveq2d 6895	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾s 𝑈))))
92	90	fveq2d 6895	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘(𝐴 ↾s 𝑈))))
93		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝐸) = (+g‘𝐸)
94	5, 93	ressplusg 17237	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+g‘𝐸) = (+g‘𝐹))
95	3, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐹))
96	34, 36	sraaddg 20800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐴))
97	27, 30	sraaddg 20800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+g‘𝐹) = (+g‘𝐶))
98	95, 96, 97	3eqtr3rd 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+g‘𝐶) = (+g‘𝐴))
99		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝐴) = (+g‘𝐴)
100	84, 99	ressplusg 17237	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+g‘𝐴) = (+g‘(𝐴 ↾s 𝑈)))
101	3, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+g‘𝐴) = (+g‘(𝐴 ↾s 𝑈)))
102	98, 101	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+g‘𝐶) = (+g‘(𝐴 ↾s 𝑈)))
103	102	oveqdr 7439	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g‘𝐶)𝑦) = (𝑥(+g‘(𝐴 ↾s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2833	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing)
106		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉)
107	26, 106	sralvec 32731	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 20722	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘𝐶)
113		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 20493	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
115	114	3expb 1120	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
116	110, 115	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
117		fedgmul.b	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118	117, 1, 3	drgextvsca 32736	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
119	43, 118	eqtr3d 2774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐵))
120	84, 75	ressvsca 17291	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘(𝐴 ↾s 𝑈)))
121	3, 120	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘(𝐴 ↾s 𝑈)))
122	5, 67	ressmulr 17254	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (.r‘𝐸) = (.r‘𝐹))
123	3, 122	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹))
124	26, 104, 4	drgextvsca 32736	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐹) = ( ·𝑠 ‘𝐶))
125	123, 118, 124	3eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·𝑠 ‘𝐵) = ( ·𝑠 ‘𝐶))
126	119, 121, 125	3eqtr3rd 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘(𝐴 ↾s 𝑈)))
127	126	oveqdr 7439	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠 ‘𝐶)𝑦) = (𝑥( ·𝑠 ‘(𝐴 ↾s 𝑈))𝑦))
128		ovexd 7446	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾s 𝑈) ∈ V)
129	87, 91, 92, 103, 116, 127, 108, 128	lindspropd 32544	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾s 𝑈)))
130	82, 129	eleqtrd 2835	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈)))
131	76, 84	lsslinds 21392	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132	131	biimpa 477	. . . . . . . . . 10 ⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
133	15, 79, 80, 130, 132	syl31anc 1373	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴))
134		eqid 2732	. . . . . . . . . . 11 ⊢ (0g‘𝐴) = (0g‘𝐴)
135		eqid 2732	. . . . . . . . . . 11 ⊢ (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
136	74, 73, 72, 75, 134, 135	islinds5 32525	. . . . . . . . . 10 ⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
137	136	biimpa 477	. . . . . . . . 9 ⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
138	15, 39, 133, 137	syl21anc 836	. . . . . . . 8 ⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
139	138	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
140		eqid 2732	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
141		fvexd 6906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) ∈ 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 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
147	142, 16	xpexd 7740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
148		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150	148, 73, 135, 149	frlmelbas 21317	. . . . . . . . . . . . . . . 16 ⊢ (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
151	146, 147, 150	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
152	145, 151	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴))))
153	152	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
154		fvexd 6906	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155	154, 147	elmapd 8836	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156	153, 155	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157	156	ffnd 6718	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
158	157	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
160	152	simprd 496	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0g‘(Scalar‘𝐴)))
161		drngring 20368	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
162	1, 161	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
163		ringmnd 20068	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164	162, 163	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
165		subrgsubg 20329	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
166	9, 165	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
167		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘𝐸) = (0g‘𝐸)
168	167	subg0cl 19016	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ 𝑉)
169	166, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝑉)
170	46, 169	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝑈)
171	5, 21, 167	ress0g 18655	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐹))
172	164, 170, 23, 171	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐹))
173	54	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐾) = (0g‘(Scalar‘𝐶)))
174	11, 167	subrg0 20330	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0g‘𝐸) = (0g‘𝐾))
175	9, 174	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾))
176	60	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
177	173, 175, 176	3eqtr4d 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(Scalar‘𝐴)))
178	172, 177	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐴)))
179	160, 178	breqtrrd 5176	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0g‘𝐹))
180	179	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0g‘𝐹))
181	140, 141, 143, 144, 158, 159, 180	fsuppcurry1 31988	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘𝐹))
182	178	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) = (0g‘(Scalar‘𝐴)))
183	181, 182	breqtrd 5174	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)))
184		eqidd 2733	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
185	156	fovcdmda 7580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186	185	anassrs 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	184, 186	fvmpt2d 7011	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188	187	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))
189	119	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐵))
190	189	oveqd 7428	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))
191	188, 190	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))
192	191	mpteq2dva 5248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))
193	192	oveq2d 7427	. . . . . . . . . 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 32740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
198	3	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199	104	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
200	117, 194, 198, 5, 199, 144	drgextgsum 32740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
201	197, 200	eqtr3d 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
202	193, 201	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
203	142	mptexd 7228	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ V)
204		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (0g‘𝐵) = (0g‘𝐵)
205	117, 5	sralvec 32731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
206	1, 104, 3, 205	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
207		lveclmod 20722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208	206, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
209	208	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
210		lmodabl 20524	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
212	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213	212, 3, 23	srasubrg 32730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
214		subrgsubg 20329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵))
216	215	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217	110	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
218	61	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219	186, 218	eleqtrd 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
220	20	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
221		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
222	220, 221	sseldd 3983	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
223	17, 111, 112, 113	lmodvscl 20493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
224	217, 219, 222, 223	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	125	oveqd 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖))
226	225	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖))
227	32	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
228	224, 226, 227	3eltr4d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) ∈ 𝑈)
229	228	fmpttd 7116	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
230	212, 23	srasca 20804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
231	5, 230	eqtrid 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
232	231	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
233		eqid 2732	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
234		ovexd 7446	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
235	20, 33	sstrd 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
236	235	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
238	236, 237	sseldd 3983	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
239	238	anassrs 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
240	212, 23	srabase 20798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241	240	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
242	239, 241	eleqtrd 2835	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
243		eqid 2732	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝐹) = (0g‘𝐹)
244		eqid 2732	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·𝑠 ‘𝐵) = ( ·𝑠 ‘𝐵)
245	144, 209, 232, 233, 234, 242, 204, 243, 244, 181	mptscmfsupp0 20542	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)) finSupp (0g‘𝐵))
246	204, 211, 144, 216, 229, 245	gsumsubgcl 19790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
247	231	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
248	25, 247	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
249	248	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250	246, 249	eleqtrd 2835	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251	250	fmpttd 7116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252	251	ffund 6721	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))))
253		fvexd 6906	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
254		fconstmpt 5738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴)))
255	254	eqeq2i 2745	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
256		ovex 7444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
257	256	rgenw 3065	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
258		mpteqb 7017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
259	257, 258	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
260	255, 259	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
261	260	necon3abii 2987	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
262		df-ov 7414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263	262	eqcomi 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265	264	eqeq1d 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
266	265	necon3abid 2977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
267	266	rexbidva 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
268		rexnal 3100	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
269	267, 268	bitr2di 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
270	261, 269	bitrid 282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
271	270	rabbidva 3439	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))})
272		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273	272	neeq1d 3000	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
274	273	dmrab 31775	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))}
275	271, 274	eqtr4di 2790	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))})
276		fvexd 6906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) ∈ V)
277		suppvalfn 8156	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))})
278	157, 147, 276, 277	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))})
279	160	fsuppimpd 9371	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) ∈ Fin)
280	278, 279	eqeltrrd 2834	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
281		dmfi 9332	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
282	280, 281	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
283	275, 282	eqeltrd 2833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin)
284		nfv 1917	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
285		nfcv 2903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
286		nfmpt1 5256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
287		nfcv 2903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0g‘(Scalar‘𝐴))})
288	286, 287	nfne 3043	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})
289	288, 285	nfrabw 3468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}
290	285, 289	nfdif 4125	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
291	290	nfcri 2890	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
292	284, 291	nfan 1902	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
293		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
294	293	eldifad 3960	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
295	293	eldifbd 3961	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
296		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297	296	mpteq2dv 5250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
298	297	neeq1d 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
299	298	elrab 3683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
300	295, 299	sylnib 327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
301	294, 300	mpnanrd 410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}))
302		nne 2944	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
303	301, 302	sylib 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
304	303, 254	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
305		ovex 7444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
306	305	rgenw 3065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
307		mpteqb 7017	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
308	306, 307	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
309	304, 308	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
310	309	r19.21bi 3248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
311	310	oveq1d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = ((0g‘(Scalar‘𝐴))( ·𝑠 ‘𝐵)𝑖))
312	117, 1, 3	drgext0g 32735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵))
313	117, 1, 3	drgext0gsca 32737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵)))
314	312, 177, 313	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
315	314	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
316	315	oveq1d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0g‘(Scalar‘𝐴))( ·𝑠 ‘𝐵)𝑖) = ((0g‘(Scalar‘𝐵))( ·𝑠 ‘𝐵)𝑖))
317	208	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod)
318	294, 242	syldanl 602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
319		eqid 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
320		eqid 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
321	233, 319, 244, 320, 204	lmod0vs 20510	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0g‘(Scalar‘𝐵))( ·𝑠 ‘𝐵)𝑖) = (0g‘𝐵))
322	317, 318, 321	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0g‘(Scalar‘𝐵))( ·𝑠 ‘𝐵)𝑖) = (0g‘𝐵))
323	311, 316, 322	3eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = (0g‘𝐵))
324	292, 323	mpteq2da 5246	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘𝐵)))
325	324	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))))
326	208, 210	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ Abel)
327		ablgrp 19655	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
328		grpmnd 18828	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
329	326, 327, 328	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
330	204	gsumz 18719	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵))
331	329, 16, 330	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵))
332	331	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵))
333	313	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (0g‘𝐵) = (0g‘(Scalar‘𝐵)))
334	325, 332, 333	3eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
335	334, 142	suppss2 8187	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
336		suppssfifsupp 9380	. . . . . . . . . . . . . 14 ⊢ ((((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ V ∧ Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∧ (0g‘(Scalar‘𝐵)) ∈ V) ∧ ({𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin ∧ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
337	203, 252, 253, 283, 335, 336	syl32anc 1378	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
338		eqidd 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))))
339		ovexd 7446	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V)
340	338, 339	fvmpt2d 7011	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
341	340	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
342	341	mpteq2dva 5248	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗)))
343	342	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
344	119	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐵))
345	43	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
346	345	oveqd 7428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))
347	346	mpteq2dva 5248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))
348	118	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
349	348	oveqd 7428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))
350	349	mpteq2dv 5250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))
351	347, 350	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))
352	351	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
353		eqidd 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
354	344, 352, 353	oveq123d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
355	201	oveq1d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
356	354, 355	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
357	356	mpteq2dva 5248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗)))
358	357	oveq2d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
359	10, 21	sraring 20814	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
360	162, 36, 359	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
361		ringcmn 20101	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
362	360, 361	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
363	162	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
364		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
365	233, 364	lbsss 20693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
366	142, 365	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
367	366, 240	sseqtrrd 4023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
368	367	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
369		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
370	368, 369	sseldd 3983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
371	21, 67	ringcl 20075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
372	363, 238, 370, 371	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
373	37	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴))
374	372, 373	eleqtrd 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
375	374	ralrimivva 3200	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
376		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))
377	376	fmpo 8056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378	375, 377	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
379	72, 73, 75, 74, 15, 156, 378, 147	lcomf 20516	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
380	72, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160	lcomfsupp 20517	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷) finSupp (0g‘𝐴))
381	74, 134, 362, 142, 16, 379, 380	gsumxp 19846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))))))
382		fedgmullem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴))
383	162	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
384	156	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
385	57, 55	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
386	385, 36	eqsstrrd 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
387	61, 386	eqsstrd 4020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
388	387, 37	sseqtrd 4022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389	388	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390	384, 389	fssd 6735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
391		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
392		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
393	390, 391, 392	fovcdmd 7581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
394	37	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
395	393, 394	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
396	238	3impb 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
397	370	3impb 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
398	21, 67	ringass 20078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
399	383, 395, 396, 397, 398	syl13anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
400	399	mpoeq3dva 7488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
401		ovexd 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
402		ovexd 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ V)
403		fnov 7542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
404	157, 403	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
405	376	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)))
406	142, 16, 401, 402, 404, 405	offval22 8076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘f (.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
407	43	ofeqd 7674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘f (.r‘𝐸) = ∘f ( ·𝑠 ‘𝐴))
408	407	oveqd 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘f (.r‘𝐸)𝐷) = (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷))
409	400, 406, 408	3eqtr2rd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))
410	409	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))
411	410	oveqd 7428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖))
412		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
413		ovexd 7446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V)
414		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
415	414	ovmpt4g 7557	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
416	412, 221, 413, 415	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
417	411, 416	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
418	417	mpteq2dva 5248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))
419	418	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))))
420	162	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
421	367	sselda 3982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
422	162	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
423	386	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
424	423, 219	sseldd 3983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
425	21, 67	ringcl 20075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
426	422, 424, 239, 425	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
427	312	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐸) = (0g‘𝐵))
428	245, 350, 427	3brtr4d 5180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸))
429	21, 167, 67, 420, 144, 421, 426, 428	gsummulc1 20132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
430	419, 429	eqtrd 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
431	144	mptexd 7228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
432	15	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
433	36	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
434	10, 431, 194, 432, 433	gsumsra 32240	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))))
435	144	mptexd 7228	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) ∈ V)
436	10, 435, 194, 432, 433	gsumsra 32240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))))
437	436	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
438	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
439	347	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))))
440	438, 439, 353	oveq123d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))
441	437, 440	eqtrd 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))
442	430, 434, 441	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))
443	442	mpteq2dva 5248	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗)))
444	443	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))))
445	381, 382, 444	3eqtr3rd 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))) = (0g‘𝐴))
446	10, 1, 9	drgext0g 32735	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐴))
447	445, 446, 312	3eqtr2d 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))) = (0g‘𝐵))
448	10, 1, 9, 11, 2, 142	drgextgsum 32740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
449	117, 1, 3, 5, 104, 142	drgextgsum 32740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
450	448, 449	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
451	358, 447, 450	3eqtr3rd 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵))
452	343, 451	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵))
453		breq1 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵))))
454		nfmpt1 5256	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
455	454	nfeq2 2920	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
456		fveq1 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗))
457	456	oveq1d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))
458	457	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))
459	455, 458	mpteq2da 5246	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗)))
460	459	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
461	460	eqeq1d 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → ((𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵) ↔ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)))
462	453, 461	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → ((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵))))
463		eqeq1 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
464	462, 463	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})) ↔ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
465	364	lbslinds 21394	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
466	465, 142	sselid 3980	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
467		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
468	233, 467, 319, 244, 204, 320	islinds5 32525	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
469	468	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
470	208, 366, 466, 469	syl21anc 836	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
471		fvexd 6906	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
472		elmapg 8835	. . . . . . . . . . . . . . . 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 836	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
475	464, 470, 474	rspcdva 3613	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
476	337, 452, 475	mp2and 697	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))
477		fconstmpt 5738	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0g‘(Scalar‘𝐵)))
478	476, 477	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0g‘(Scalar‘𝐵))))
479		ovex 7444	. . . . . . . . . . . . 13 ⊢ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V
480	479	rgenw 3065	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V
481		mpteqb 7017	. . . . . . . . . . . 12 ⊢ (∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵))))
482	480, 481	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0g‘(Scalar‘𝐵))) ↔ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
483	478, 482	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
484	483	r19.21bi 3248	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
485	312, 446, 313	3eqtr3rd 2781	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) = (0g‘𝐴))
486	485	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘(Scalar‘𝐵)) = (0g‘𝐴))
487	202, 484, 486	3eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴))
488	183, 487	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)))
489	186	fmpttd 7116	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
490		fvexd 6906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
491	490, 144	elmapd 8836	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
492	489, 491	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋))
493		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
494	493	breq1d 5158	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴))))
495		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
496		nfmpt1 5256	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
497	496	nfeq2 2920	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
498	495, 497	nfan 1902	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
499		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
500	499	fveq1d 6893	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
501	500	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))
502	498, 501	mpteq2da 5246	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖)))
503	502	oveq2d 7427	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))))
504	503	eqeq1d 2734	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴) ↔ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)))
505	494, 504	anbi12d 631	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴))))
506	493	eqeq1d 2734	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))})))
507	505, 506	imbi12d 344	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
508	492, 507	rspcdv 3604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
509	139, 488, 508	mp2d 49	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
510	509, 254	eqtrdi 2788	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
511	510, 308	sylib 217	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
512	511	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
513		eqidd 2733	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴)))
514		fvexd 6906	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
515		fvexd 6906	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
516	157, 513, 514, 515	fnmpoovd 8075	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
517	512, 516	mpbird 256	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
518		fconstmpo 7527	. 2 ⊢ ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴)))
519	517, 518	eqtr4di 2790	1 ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3432  Vcvv 3474   ∖ cdif 3945   ⊆ wss 3948  {csn 4628  ⟨cop 4634   class class class wbr 5148   ↦ cmpt 5231   × cxp 5674  dom cdm 5676  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  (class class class)co 7411   ∈ cmpo 7413   ∘_f cof 7670   supp csupp 8148   ↑_m cmap 8822  Fincfn 8941   finSupp cfsupp 9363  Basecbs 17146   ↾_s cress 17175  +_gcplusg 17199  ._rcmulr 17200  Scalarcsca 17202   ·_𝑠 cvsca 17203  0_gc0g 17387   Σ_g cgsu 17388  Mndcmnd 18627  Grpcgrp 18821  SubGrpcsubg 19002  CMndccmn 19650  Abelcabl 19651  Ringcrg 20058  SubRingcsubrg 20319  DivRingcdr 20361  LModclmod 20475  LSubSpclss 20547  LBasisclbs 20690  LVecclvec 20718  subringAlg csra 20787   freeLMod cfrlm 21307  LIndSclinds 21366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-fz 13487  df-fzo 13630  df-seq 13969  df-hash 14293  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ds 17221  df-hom 17223  df-cco 17224  df-0g 17389  df-gsum 17390  df-prds 17395  df-pws 17397  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-mhm 18673  df-submnd 18674  df-grp 18824  df-minusg 18825  df-sbg 18826  df-mulg 18953  df-subg 19005  df-ghm 19092  df-cntz 19183  df-cmn 19652  df-abl 19653  df-mgp 19990  df-ur 20007  df-ring 20060  df-nzr 20296  df-subrg 20321  df-drng 20363  df-lmod 20477  df-lss 20548  df-lsp 20588  df-lmhm 20638  df-lbs 20691  df-lvec 20719  df-sra 20791  df-rgmod 20792  df-dsmm 21293  df-frlm 21308  df-uvc 21344  df-lindf 21367  df-linds 21368

This theorem is referenced by:  fedgmul  32775