Theorem fedgmullem2 32715

Description: Lemma for fedgmul 32716. (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 20345	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
7	6	biimpa 478	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
8	3, 4, 7	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
9	8	simpld 496	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
10		fedgmul.a	. . . . . . . . . . . 12 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
11		fedgmul.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (𝐸 ↾s 𝑉)
12	10, 11	sralvec 32675	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ DivRing ∧ 𝐾 ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
13	1, 2, 9, 12	syl3anc 1372	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ LVec)
14		lveclmod 20717	. . . . . . . . . 10 ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ LMod)
16		fedgmullem.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
17		eqid 2733	. . . . . . . . . . . 12 ⊢ (Base‘𝐶) = (Base‘𝐶)
18		eqid 2733	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
19	17, 18	lbsss 20688	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
20	16, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
21		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
22	21	subrgss 20320	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
23	3, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
24	5, 21	ressbas2 17182	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
26		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
28		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
29	28	subrgss 20320	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
30	4, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
31	27, 30	srabase 20792	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
32	25, 31	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
33	32, 23	eqsstrrd 4022	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
34	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
35	21	subrgss 20320	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
36	9, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
37	34, 36	srabase 20792	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
38	33, 37	sseqtrd 4023	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐴))
39	20, 38	sstrd 3993	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐴))
40	34, 3, 36	srasubrg 32674	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
41		subrgsubg 20325	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubRing‘𝐴) → 𝑈 ∈ (SubGrp‘𝐴))
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐴))
43	10, 1, 9	drgextvsca 32678	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
44	43	oveqdr 7437	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) = (𝑥( ·𝑠 ‘𝐴)𝑦))
45	3	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ (SubRing‘𝐸))
46	8	simprd 497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
47	46	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 ⊆ 𝑈)
48		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐴)))
49		ressabs 17194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
50	3, 46, 49	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
51	5	oveq1i 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉)
52	50, 51, 11	3eqtr4g 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾)
53	27, 30	srasca 20798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
54	52, 53	eqtr3d 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
55	54	fveq2d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
56	11, 21	ressbas2 17182	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
57	36, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
58	34, 36	srasca 20798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
59	11, 58	eqtrid 2785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
60	52, 53, 59	3eqtr3rd 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
61	60	fveq2d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
62	55, 57, 61	3eqtr4d 2783	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐴)))
63	62	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑉 = (Base‘(Scalar‘𝐴)))
64	48, 63	eleqtrrd 2837	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑉)
65	47, 64	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
66		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
67		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (.r‘𝐸) = (.r‘𝐸)
68	67	subrgmcl 20331	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈)
69	45, 65, 66, 68	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑈)
70	44, 69	eqeltrrd 2835	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ 𝑈)) → (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)
71	70	ralrimivva 3201	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)
72		eqid 2733	. . . . . . . . . . . . 13 ⊢ (Scalar‘𝐴) = (Scalar‘𝐴)
73		eqid 2733	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))
74		eqid 2733	. . . . . . . . . . . . 13 ⊢ (Base‘𝐴) = (Base‘𝐴)
75		eqid 2733	. . . . . . . . . . . . 13 ⊢ ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐴)
76		eqid 2733	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝐴) = (LSubSp‘𝐴)
77	72, 73, 74, 75, 76	islss4 20573	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ LMod → (𝑈 ∈ (LSubSp‘𝐴) ↔ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)))
78	77	biimpar 479	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ (𝑈 ∈ (SubGrp‘𝐴) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝐴))∀𝑦 ∈ 𝑈 (𝑥( ·𝑠 ‘𝐴)𝑦) ∈ 𝑈)) → 𝑈 ∈ (LSubSp‘𝐴))
79	15, 42, 71, 78	syl12anc 836	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐴))
80	20, 32	sseqtrrd 4024	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ 𝑈)
81	18	lbslinds 21388	. . . . . . . . . . . 12 ⊢ (LBasis‘𝐶) ⊆ (LIndS‘𝐶)
82	81, 16	sselid 3981	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
83	23, 37	sseqtrd 4023	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐴))
84		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾s 𝑈) = (𝐴 ↾s 𝑈)
85	84, 74	ressbas2 17182	. . . . . . . . . . . . . 14 ⊢ (𝑈 ⊆ (Base‘𝐴) → 𝑈 = (Base‘(𝐴 ↾s 𝑈)))
86	83, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 = (Base‘(𝐴 ↾s 𝑈)))
87	25, 86, 31	3eqtr3rd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐶) = (Base‘(𝐴 ↾s 𝑈)))
88	84, 72	resssca 17288	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈)))
89	3, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘(𝐴 ↾s 𝑈)))
90	60, 89	eqtr3d 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝐶) = (Scalar‘(𝐴 ↾s 𝑈)))
91	90	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘(𝐴 ↾s 𝑈))))
92	90	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘(𝐴 ↾s 𝑈))))
93		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝐸) = (+g‘𝐸)
94	5, 93	ressplusg 17235	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+g‘𝐸) = (+g‘𝐹))
95	3, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐹))
96	34, 36	sraaddg 20794	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐴))
97	27, 30	sraaddg 20794	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (+g‘𝐹) = (+g‘𝐶))
98	95, 96, 97	3eqtr3rd 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+g‘𝐶) = (+g‘𝐴))
99		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝐴) = (+g‘𝐴)
100	84, 99	ressplusg 17235	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (+g‘𝐴) = (+g‘(𝐴 ↾s 𝑈)))
101	3, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+g‘𝐴) = (+g‘(𝐴 ↾s 𝑈)))
102	98, 101	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (+g‘𝐶) = (+g‘(𝐴 ↾s 𝑈)))
103	102	oveqdr 7437	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(+g‘𝐶)𝑦) = (𝑥(+g‘(𝐴 ↾s 𝑈))𝑦))
104		fedgmul.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ DivRing)
105	52, 2	eqeltrd 2834	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing)
106		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉)
107	26, 106	sralvec 32675	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
108	104, 105, 4, 107	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
109		lveclmod 20717	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
111		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
112		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘𝐶)
113		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
114	17, 111, 112, 113	lmodvscl 20489	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥( ·𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
115	114	3expb 1121	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
116	110, 115	sylan 581	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠 ‘𝐶)𝑦) ∈ (Base‘𝐶))
117		fedgmul.b	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
118	117, 1, 3	drgextvsca 32678	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
119	43, 118	eqtr3d 2775	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐵))
120	84, 75	ressvsca 17289	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘(𝐴 ↾s 𝑈)))
121	3, 120	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘(𝐴 ↾s 𝑈)))
122	5, 67	ressmulr 17252	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (.r‘𝐸) = (.r‘𝐹))
123	3, 122	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹))
124	26, 104, 4	drgextvsca 32678	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐹) = ( ·𝑠 ‘𝐶))
125	123, 118, 124	3eqtr3d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ·𝑠 ‘𝐵) = ( ·𝑠 ‘𝐶))
126	119, 121, 125	3eqtr3rd 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘(𝐴 ↾s 𝑈)))
127	126	oveqdr 7437	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥( ·𝑠 ‘𝐶)𝑦) = (𝑥( ·𝑠 ‘(𝐴 ↾s 𝑈))𝑦))
128		ovexd 7444	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ↾s 𝑈) ∈ V)
129	87, 91, 92, 103, 116, 127, 108, 128	lindspropd 32499	. . . . . . . . . . 11 ⊢ (𝜑 → (LIndS‘𝐶) = (LIndS‘(𝐴 ↾s 𝑈)))
130	82, 129	eleqtrd 2836	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈)))
131	76, 84	lsslinds 21386	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) → (𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈)) ↔ 𝑋 ∈ (LIndS‘𝐴)))
132	131	biimpa 478	. . . . . . . . . 10 ⊢ (((𝐴 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝐴) ∧ 𝑋 ⊆ 𝑈) ∧ 𝑋 ∈ (LIndS‘(𝐴 ↾s 𝑈))) → 𝑋 ∈ (LIndS‘𝐴))
133	15, 79, 80, 130, 132	syl31anc 1374	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐴))
134		eqid 2733	. . . . . . . . . . 11 ⊢ (0g‘𝐴) = (0g‘𝐴)
135		eqid 2733	. . . . . . . . . . 11 ⊢ (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴))
136	74, 73, 72, 75, 134, 135	islinds5 32480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) → (𝑋 ∈ (LIndS‘𝐴) ↔ ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
137	136	biimpa 478	. . . . . . . . 9 ⊢ (((𝐴 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐴)) ∧ 𝑋 ∈ (LIndS‘𝐴)) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
138	15, 39, 133, 137	syl21anc 837	. . . . . . . 8 ⊢ (𝜑 → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
139	138	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑤 ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋)((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})))
140		eqid 2733	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
141		fvexd 6907	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) ∈ V)
142		fedgmullem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
143	142	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ∈ (LBasis‘𝐵))
144	16	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
145		fedgmullem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))
146		fvexd 6907	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Scalar‘𝐴) ∈ V)
147	142, 16	xpexd 7738	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
148		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)) = ((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))
149		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) = (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))
150	148, 73, 135, 149	frlmelbas 21311	. . . . . . . . . . . . . . . 16 ⊢ (((Scalar‘𝐴) ∈ V ∧ (𝑌 × 𝑋) ∈ V) → (𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))) ↔ (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ 𝑊 finSupp (0g‘(Scalar‘𝐴)))))
151	146, 147, 150	syl2anc 585	. . . . . . . . . . . . . . 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 496	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
154		fvexd 6907	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ∈ V)
155	154, 147	elmapd 8834	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
156	153, 155	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
157	156	ffnd 6719	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 Fn (𝑌 × 𝑋))
158	157	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 Fn (𝑌 × 𝑋))
159		simpr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
160	152	simprd 497	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 finSupp (0g‘(Scalar‘𝐴)))
161		drngring 20364	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
162	1, 161	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ∈ Ring)
163		ringmnd 20066	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
164	162, 163	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Mnd)
165		subrgsubg 20325	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ∈ (SubGrp‘𝐸))
166	9, 165	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ∈ (SubGrp‘𝐸))
167		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘𝐸) = (0g‘𝐸)
168	167	subg0cl 19014	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ 𝑉)
169	166, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝑉)
170	46, 169	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝑈)
171	5, 21, 167	ress0g 18653	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐹))
172	164, 170, 23, 171	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐹))
173	54	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐾) = (0g‘(Scalar‘𝐶)))
174	11, 167	subrg0 20326	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0g‘𝐸) = (0g‘𝐾))
175	9, 174	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾))
176	60	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
177	173, 175, 176	3eqtr4d 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(Scalar‘𝐴)))
178	172, 177	eqtr3d 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐴)))
179	160, 178	breqtrrd 5177	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 finSupp (0g‘𝐹))
180	179	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑊 finSupp (0g‘𝐹))
181	140, 141, 143, 144, 158, 159, 180	fsuppcurry1 31950	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘𝐹))
182	178	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐹) = (0g‘(Scalar‘𝐴)))
183	181, 182	breqtrd 5175	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)))
184		eqidd 2734	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
185	156	fovcdmda 7578	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
186	185	anassrs 469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐴)))
187	184, 186	fvmpt2d 7012	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖) = (𝑗𝑊𝑖))
188	187	oveq1d 7424	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))
189	119	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐵))
190	189	oveqd 7426	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))
191	188, 190	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))
192	191	mpteq2dva 5249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))
193	192	oveq2d 7425	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
194	1	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ DivRing)
195	9	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ∈ (SubRing‘𝐸))
196	2	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐾 ∈ DivRing)
197	10, 194, 195, 11, 196, 144	drgextgsum 32682	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
198	3	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
199	104	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 ∈ DivRing)
200	117, 194, 198, 5, 199, 144	drgextgsum 32682	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
201	197, 200	eqtr3d 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
202	193, 201	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
203	142	mptexd 7226	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ V)
204		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (0g‘𝐵) = (0g‘𝐵)
205	117, 5	sralvec 32675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐵 ∈ LVec)
206	1, 104, 3, 205	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ LVec)
207		lveclmod 20717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ LVec → 𝐵 ∈ LMod)
208	206, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ LMod)
209	208	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ LMod)
210		lmodabl 20519	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ LMod → 𝐵 ∈ Abel)
211	209, 210	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐵 ∈ Abel)
212	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
213	212, 3, 23	srasubrg 32674	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
214		subrgsubg 20325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 ∈ (SubRing‘𝐵) → 𝑈 ∈ (SubGrp‘𝐵))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐵))
216	215	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝐵))
217	110	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
218	61	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
219	186, 218	eleqtrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)))
220	20	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
221		simpr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
222	220, 221	sseldd 3984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
223	17, 111, 112, 113	lmodvscl 20489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ LMod ∧ (𝑗𝑊𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
224	217, 219, 222, 223	syl3anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
225	125	oveqd 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖))
226	225	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐶)𝑖))
227	32	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
228	224, 226, 227	3eltr4d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) ∈ 𝑈)
229	228	fmpttd 7115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)):𝑋⟶𝑈)
230	212, 23	srasca 20798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
231	5, 230	eqtrid 2785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
232	231	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐹 = (Scalar‘𝐵))
233		eqid 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐵) = (Base‘𝐵)
234		ovexd 7444	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
235	20, 33	sstrd 3993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
236	235	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝐸))
237		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
238	236, 237	sseldd 3984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ (Base‘𝐸))
239	238	anassrs 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
240	212, 23	srabase 20792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
241	240	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐵))
242	239, 241	eleqtrd 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
243		eqid 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝐹) = (0g‘𝐹)
244		eqid 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ ( ·𝑠 ‘𝐵) = ( ·𝑠 ‘𝐵)
245	144, 209, 232, 233, 234, 242, 204, 243, 244, 181	mptscmfsupp0 20537	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)) finSupp (0g‘𝐵))
246	204, 211, 144, 216, 229, 245	gsumsubgcl 19788	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ 𝑈)
247	231	fveq2d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐹) = (Base‘(Scalar‘𝐵)))
248	25, 247	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = (Base‘(Scalar‘𝐵)))
249	248	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 = (Base‘(Scalar‘𝐵)))
250	246, 249	eleqtrd 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ (Base‘(Scalar‘𝐵)))
251	250	fmpttd 7115	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵)))
252	251	ffund 6722	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))))
253		fvexd 6907	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
254		fconstmpt 5739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × {(0g‘(Scalar‘𝐴))}) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴)))
255	254	eqeq2i 2746	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
256		ovex 7442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘𝑊𝑖) ∈ V
257	256	rgenw 3066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V
258		mpteqb 7018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) ∈ V → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
259	257, 258	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
260	255, 259	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
261	260	necon3abii 2988	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
262		df-ov 7412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘𝑊𝑖) = (𝑊‘⟨𝑘, 𝑖⟩)
263	262	eqcomi 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖)
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊‘⟨𝑘, 𝑖⟩) = (𝑘𝑊𝑖))
265	264	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) = (0g‘(Scalar‘𝐴)) ↔ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
266	265	necon3abid 2978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
267	266	rexbidva 3177	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴))))
268		rexnal 3101	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ 𝑋 ¬ (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)))
269	267, 268	bitr2di 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (¬ ∀𝑖 ∈ 𝑋 (𝑘𝑊𝑖) = (0g‘(Scalar‘𝐴)) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
270	261, 269	bitrid 283	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
271	270	rabbidva 3440	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))})
272		fveq2 6892	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → (𝑊‘𝑧) = (𝑊‘⟨𝑘, 𝑖⟩))
273	272	neeq1d 3001	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑘, 𝑖⟩ → ((𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴)) ↔ (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))))
274	273	dmrab 31737	. . . . . . . . . . . . . . . 16 ⊢ dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} = {𝑘 ∈ 𝑌 ∣ ∃𝑖 ∈ 𝑋 (𝑊‘⟨𝑘, 𝑖⟩) ≠ (0g‘(Scalar‘𝐴))}
275	271, 274	eqtr4di 2791	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} = dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))})
276		fvexd 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) ∈ V)
277		suppvalfn 8154	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 Fn (𝑌 × 𝑋) ∧ (𝑌 × 𝑋) ∈ V ∧ (0g‘(Scalar‘𝐴)) ∈ V) → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))})
278	157, 147, 276, 277	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) = {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))})
279	160	fsuppimpd 9369	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 supp (0g‘(Scalar‘𝐴))) ∈ Fin)
280	278, 279	eqeltrrd 2835	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
281		dmfi 9330	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
282	280, 281	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom {𝑧 ∈ (𝑌 × 𝑋) ∣ (𝑊‘𝑧) ≠ (0g‘(Scalar‘𝐴))} ∈ Fin)
283	275, 282	eqeltrd 2834	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ∈ Fin)
284		nfv 1918	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝜑
285		nfcv 2904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖𝑌
286		nfmpt1 5257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖))
287		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑖(𝑋 × {(0g‘(Scalar‘𝐴))})
288	286, 287	nfne 3044	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})
289	288, 285	nfrabw 3469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑖{𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}
290	285, 289	nfdif 4126	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑖(𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
291	290	nfcri 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
292	284, 291	nfan 1903	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
293		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})}))
294	293	eldifad 3961	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → 𝑗 ∈ 𝑌)
295	293	eldifbd 3962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ 𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
296		oveq1 7416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑗 → (𝑘𝑊𝑖) = (𝑗𝑊𝑖))
297	296	mpteq2dv 5251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑗 → (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
298	297	neeq1d 3001	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑗 → ((𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
299	298	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})} ↔ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
300	295, 299	sylnib 328	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑗 ∈ 𝑌 ∧ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})))
301	294, 300	mpnanrd 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → ¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}))
302		nne 2945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
303	301, 302	sylib 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))
304	303, 254	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
305		ovex 7442	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗𝑊𝑖) ∈ V
306	305	rgenw 3066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) ∈ V
307		mpteqb 7018	. . . . . . . . . . . . . . . . . . . . . . 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 3249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
311	310	oveq1d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = ((0g‘(Scalar‘𝐴))( ·𝑠 ‘𝐵)𝑖))
312	117, 1, 3	drgext0g 32677	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵))
313	117, 1, 3	drgext0gsca 32679	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵)))
314	312, 177, 313	3eqtr3d 2781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
315	314	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐵)))
316	315	oveq1d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0g‘(Scalar‘𝐴))( ·𝑠 ‘𝐵)𝑖) = ((0g‘(Scalar‘𝐵))( ·𝑠 ‘𝐵)𝑖))
317	208	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝐵 ∈ LMod)
318	294, 242	syldanl 603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐵))
319		eqid 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Scalar‘𝐵) = (Scalar‘𝐵)
320		eqid 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0g‘(Scalar‘𝐵)) = (0g‘(Scalar‘𝐵))
321	233, 319, 244, 320, 204	lmod0vs 20505	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ LMod ∧ 𝑖 ∈ (Base‘𝐵)) → ((0g‘(Scalar‘𝐵))( ·𝑠 ‘𝐵)𝑖) = (0g‘𝐵))
322	317, 318, 321	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((0g‘(Scalar‘𝐵))( ·𝑠 ‘𝐵)𝑖) = (0g‘𝐵))
323	311, 316, 322	3eqtrd 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖) = (0g‘𝐵))
324	292, 323	mpteq2da 5247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘𝐵)))
325	324	oveq2d 7425	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))))
326	208, 210	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ Abel)
327		ablgrp 19653	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Abel → 𝐵 ∈ Grp)
328		grpmnd 18826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Grp → 𝐵 ∈ Mnd)
329	326, 327, 328	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ Mnd)
330	204	gsumz 18717	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Mnd ∧ 𝑋 ∈ (LBasis‘𝐶)) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵))
331	329, 16, 330	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵))
332	331	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ (0g‘𝐵))) = (0g‘𝐵))
333	313	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (0g‘𝐵) = (0g‘(Scalar‘𝐵)))
334	325, 332, 333	3eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
335	334, 142	suppss2 8185	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) supp (0g‘(Scalar‘𝐵))) ⊆ {𝑘 ∈ 𝑌 ∣ (𝑖 ∈ 𝑋 ↦ (𝑘𝑊𝑖)) ≠ (𝑋 × {(0g‘(Scalar‘𝐴))})})
336		suppssfifsupp 9378	. . . . . . . . . . . . . 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 1379	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)))
338		eqidd 2734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))))
339		ovexd 7444	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V)
340	338, 339	fvmpt2d 7012	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
341	340	oveq1d 7424	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
342	341	mpteq2dva 5249	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗)))
343	342	oveq2d 7425	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
344	119	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ( ·𝑠 ‘𝐴) = ( ·𝑠 ‘𝐵))
345	43	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
346	345	oveqd 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))
347	346	mpteq2dva 5249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))
348	118	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
349	348	oveqd 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) = ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))
350	349	mpteq2dv 5251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))
351	347, 350	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))
352	351	oveq2d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
353		eqidd 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 = 𝑗)
354	344, 352, 353	oveq123d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
355	201	oveq1d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
356	354, 355	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗) = ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))
357	356	mpteq2dva 5249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗)) = (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗)))
358	357	oveq2d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
359	10, 21	sraring 20808	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ Ring ∧ 𝑉 ⊆ (Base‘𝐸)) → 𝐴 ∈ Ring)
360	162, 36, 359	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ Ring)
361		ringcmn 20099	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
362	360, 361	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ CMnd)
363	162	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝐸 ∈ Ring)
364		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
365	233, 364	lbsss 20688	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
366	142, 365	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
367	366, 240	sseqtrrd 4024	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
368	367	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑌 ⊆ (Base‘𝐸))
369		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ 𝑌)
370	368, 369	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑗 ∈ (Base‘𝐸))
371	21, 67	ringcl 20073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
372	363, 238, 370, 371	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
373	37	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘𝐸) = (Base‘𝐴))
374	372, 373	eleqtrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
375	374	ralrimivva 3201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
376		fedgmullem.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))
377	376	fmpo 8054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
378	375, 377	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
379	72, 73, 75, 74, 15, 156, 378, 147	lcomf 20511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐴))
380	72, 73, 75, 74, 15, 156, 378, 147, 134, 135, 160	lcomfsupp 20512	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷) finSupp (0g‘𝐴))
381	74, 134, 362, 142, 16, 379, 380	gsumxp 19844	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))))))
382		fedgmullem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴))
383	162	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
384	156	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
385	57, 55	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
386	385, 36	eqsstrrd 4022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
387	61, 386	eqsstrd 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
388	387, 37	sseqtrd 4023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
389	388	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐴))
390	384, 389	fssd 6736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑊:(𝑌 × 𝑋)⟶(Base‘𝐴))
391		simp2 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
392		simp3 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
393	390, 391, 392	fovcdmd 7579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐴))
394	37	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
395	393, 394	eleqtrrd 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
396	238	3impb 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
397	370	3impb 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
398	21, 67	ringass 20076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐸 ∈ Ring ∧ ((𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
399	383, 395, 396, 397, 398	syl13anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
400	399	mpoeq3dva 7486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
401		ovexd 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ V)
402		ovexd 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ V)
403		fnov 7540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑊 Fn (𝑌 × 𝑋) ↔ 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
404	157, 403	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑊 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
405	376	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)))
406	142, 16, 401, 402, 404, 405	offval22 8074	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘f (.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
407	43	ofeqd 7672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∘f (.r‘𝐸) = ∘f ( ·𝑠 ‘𝐴))
408	407	oveqd 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑊 ∘f (.r‘𝐸)𝐷) = (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷))
409	400, 406, 408	3eqtr2rd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))
410	409	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))
411	410	oveqd 7426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖))
412		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
413		ovexd 7444	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V)
414		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
415	414	ovmpt4g 7555	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
416	412, 221, 413, 415	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
417	411, 416	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖) = (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))
418	417	mpteq2dva 5249	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)))
419	418	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))))
420	162	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
421	367	sselda 3983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
422	162	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
423	386	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
424	423, 219	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗𝑊𝑖) ∈ (Base‘𝐸))
425	21, 67	ringcl 20073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐸 ∈ Ring ∧ (𝑗𝑊𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
426	422, 424, 239, 425	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝑗𝑊𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
427	312	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘𝐸) = (0g‘𝐵))
428	245, 350, 427	3brtr4d 5181	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸))
429	21, 167, 67, 420, 144, 421, 426, 428	gsummulc1 20128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝑗𝑊𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
430	419, 429	eqtrd 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
431	144	mptexd 7226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖)) ∈ V)
432	15	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐴 ∈ LMod)
433	36	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑉 ⊆ (Base‘𝐸))
434	10, 431, 194, 432, 433	gsumsra 32199	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))))
435	144	mptexd 7226	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)) ∈ V)
436	10, 435, 194, 432, 433	gsumsra 32199	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))))
437	436	oveq1d 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
438	43	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
439	347	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖))))
440	438, 439, 353	oveq123d 7430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))
441	437, 440	eqtrd 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))
442	430, 434, 441	3eqtr3d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))) = ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))
443	442	mpteq2dva 5249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖)))) = (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗)))
444	443	oveq2d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)𝑖))))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))))
445	381, 382, 444	3eqtr3rd 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))) = (0g‘𝐴))
446	10, 1, 9	drgext0g 32677	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐴))
447	445, 446, 312	3eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐴)𝑖)))( ·𝑠 ‘𝐴)𝑗))) = (0g‘𝐵))
448	10, 1, 9, 11, 2, 142	drgextgsum 32682	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
449	117, 1, 3, 5, 104, 142	drgextgsum 32682	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
450	448, 449	eqtr3d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))))
451	358, 447, 450	3eqtr3rd 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵))
452	343, 451	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵))
453		breq1 5152	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑏 finSupp (0g‘(Scalar‘𝐵)) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵))))
454		nfmpt1 5257	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
455	454	nfeq2 2921	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))
456		fveq1 6891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑏‘𝑗) = ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗))
457	456	oveq1d 7424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))
458	457	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∧ 𝑗 ∈ 𝑌) → ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗) = (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))
459	455, 458	mpteq2da 5247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗)))
460	459	oveq2d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
461	460	eqeq1d 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → ((𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵) ↔ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)))
462	453, 461	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → ((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) ↔ ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵))))
463		eqeq1 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
464	462, 463	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) → (((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})) ↔ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
465	364	lbslinds 21388	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘𝐵) ⊆ (LIndS‘𝐵)
466	465, 142	sselid 3981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (LIndS‘𝐵))
467		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))
468	233, 467, 319, 244, 204, 320	islinds5 32480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) → (𝑌 ∈ (LIndS‘𝐵) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))}))))
469	468	biimpa 478	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ LMod ∧ 𝑌 ⊆ (Base‘𝐵)) ∧ 𝑌 ∈ (LIndS‘𝐵)) → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
470	208, 366, 466, 469	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑏 ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌)((𝑏 finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝑏‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → 𝑏 = (𝑌 × {(0g‘(Scalar‘𝐵))})))
471		fvexd 6907	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘(Scalar‘𝐵)) ∈ V)
472		elmapg 8833	. . . . . . . . . . . . . . . 16 ⊢ (((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) → ((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌) ↔ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))))
473	472	biimpar 479	. . . . . . . . . . . . . . 15 ⊢ ((((Base‘(Scalar‘𝐵)) ∈ V ∧ 𝑌 ∈ (LBasis‘𝐵)) ∧ (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))):𝑌⟶(Base‘(Scalar‘𝐵))) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
474	471, 142, 251, 473	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) ∈ ((Base‘(Scalar‘𝐵)) ↑m 𝑌))
475	464, 470, 474	rspcdva 3614	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) finSupp (0g‘(Scalar‘𝐵)) ∧ (𝐵 Σg (𝑗 ∈ 𝑌 ↦ (((𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))))‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (0g‘𝐵)) → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))})))
476	337, 452, 475	mp2and 698	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑌 × {(0g‘(Scalar‘𝐵))}))
477		fconstmpt 5739	. . . . . . . . . . . 12 ⊢ (𝑌 × {(0g‘(Scalar‘𝐵))}) = (𝑗 ∈ 𝑌 ↦ (0g‘(Scalar‘𝐵)))
478	476, 477	eqtrdi 2789	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖)))) = (𝑗 ∈ 𝑌 ↦ (0g‘(Scalar‘𝐵))))
479		ovex 7442	. . . . . . . . . . . . 13 ⊢ (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V
480	479	rgenw 3066	. . . . . . . . . . . 12 ⊢ ∀𝑗 ∈ 𝑌 (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) ∈ V
481		mpteqb 7018	. . . . . . . . . . . 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 3249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐵 Σg (𝑖 ∈ 𝑋 ↦ ((𝑗𝑊𝑖)( ·𝑠 ‘𝐵)𝑖))) = (0g‘(Scalar‘𝐵)))
485	312, 446, 313	3eqtr3rd 2782	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) = (0g‘𝐴))
486	485	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (0g‘(Scalar‘𝐵)) = (0g‘𝐴))
487	202, 484, 486	3eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴))
488	183, 487	jca 513	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)))
489	186	fmpttd 7115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴)))
490		fvexd 6907	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐴)) ∈ V)
491	490, 144	elmapd 8834	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)):𝑋⟶(Base‘(Scalar‘𝐴))))
492	489, 491	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) ∈ ((Base‘(Scalar‘𝐴)) ↑m 𝑋))
493		simpr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
494	493	breq1d 5159	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 finSupp (0g‘(Scalar‘𝐴)) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴))))
495		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑗 ∈ 𝑌)
496		nfmpt1 5257	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
497	496	nfeq2 2921	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))
498	495, 497	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
499		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)))
500	499	fveq1d 6894	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑤‘𝑖) = ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖))
501	500	oveq1d 7424	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖) = (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))
502	498, 501	mpteq2da 5247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖)))
503	502	oveq2d 7425	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))))
504	503	eqeq1d 2735	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴) ↔ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)))
505	494, 504	anbi12d 632	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → ((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) ↔ ((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴))))
506	493	eqeq1d 2735	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))}) ↔ (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))})))
507	505, 506	imbi12d 345	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑤 = (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))) → (((𝑤 finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ ((𝑤‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → 𝑤 = (𝑋 × {(0g‘(Scalar‘𝐴))})) ↔ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) finSupp (0g‘(Scalar‘𝐴)) ∧ (𝐴 Σg (𝑖 ∈ 𝑋 ↦ (((𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖))‘𝑖)( ·𝑠 ‘𝐴)𝑖))) = (0g‘𝐴)) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑋 × {(0g‘(Scalar‘𝐴))}))))
508	492, 507	rspcdv 3605	. . . . . . 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 2789	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (𝑗𝑊𝑖)) = (𝑖 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
511	510, 308	sylib 217	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
512	511	ralrimiva 3147	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴)))
513		eqidd 2734	. . . 4 ⊢ ((𝑗 = 𝑘 ∧ 𝑖 = 𝑙) → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐴)))
514		fvexd 6907	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
515		fvexd 6907	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌 ∧ 𝑙 ∈ 𝑋) → (0g‘(Scalar‘𝐴)) ∈ V)
516	157, 513, 514, 515	fnmpoovd 8073	. . 3 ⊢ (𝜑 → (𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))) ↔ ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑗𝑊𝑖) = (0g‘(Scalar‘𝐴))))
517	512, 516	mpbird 257	. 2 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴))))
518		fconstmpo 7525	. 2 ⊢ ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}) = (𝑘 ∈ 𝑌, 𝑙 ∈ 𝑋 ↦ (0g‘(Scalar‘𝐴)))
519	517, 518	eqtr4di 2791	1 ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  {crab 3433  Vcvv 3475   ∖ cdif 3946   ⊆ wss 3949  {csn 4629  ⟨cop 4635   class class class wbr 5149   ↦ cmpt 5232   × cxp 5675  dom cdm 5677  Fun wfun 6538   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544  (class class class)co 7409   ∈ cmpo 7411   ∘_f cof 7668   supp csupp 8146   ↑_m cmap 8820  Fincfn 8939   finSupp cfsupp 9361  Basecbs 17144   ↾_s cress 17173  +_gcplusg 17197  ._rcmulr 17198  Scalarcsca 17200   ·_𝑠 cvsca 17201  0_gc0g 17385   Σ_g cgsu 17386  Mndcmnd 18625  Grpcgrp 18819  SubGrpcsubg 19000  CMndccmn 19648  Abelcabl 19649  Ringcrg 20056  SubRingcsubrg 20315  DivRingcdr 20357  LModclmod 20471  LSubSpclss 20542  LBasisclbs 20685  LVecclvec 20713  subringAlg csra 20781   freeLMod cfrlm 21301  LIndSclinds 21360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-hom 17221  df-cco 17222  df-0g 17387  df-gsum 17388  df-prds 17393  df-pws 17395  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-submnd 18672  df-grp 18822  df-minusg 18823  df-sbg 18824  df-mulg 18951  df-subg 19003  df-ghm 19090  df-cntz 19181  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-nzr 20292  df-subrg 20317  df-drng 20359  df-lmod 20473  df-lss 20543  df-lsp 20583  df-lmhm 20633  df-lbs 20686  df-lvec 20714  df-sra 20785  df-rgmod 20786  df-dsmm 21287  df-frlm 21302  df-uvc 21338  df-lindf 21361  df-linds 21362

This theorem is referenced by:  fedgmul  32716