Theorem fedgmullem1 33618

Description: Lemma for fedgmul 33620. (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‘𝐵))
fedgmullem1.a	⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴))
fedgmullem1.l	⊢ (𝜑 → 𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
fedgmullem1.1	⊢ (𝜑 → 𝐿 finSupp (0g‘(Scalar‘𝐵)))
fedgmullem1.z	⊢ (𝜑 → 𝑍 = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
fedgmullem1.g	⊢ (𝜑 → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
fedgmullem1.2	⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)))
fedgmullem1.3	⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))

Assertion

Ref	Expression
fedgmullem1	⊢ (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷))))

Distinct variable groups:   𝐴,𝑖,𝑗   𝐵,𝑗   𝐶,𝑖,𝑗   𝐷,𝑖,𝑗   𝑖,𝐸,𝑗   𝑖,𝐺,𝑗   𝑖,𝐻,𝑗   𝑗,𝐿   𝑈,𝑖   𝑖,𝑋,𝑗   𝑖,𝑌,𝑗   𝜑,𝑖,𝑗

Allowed substitution hints:   𝐵(𝑖)   𝑈(𝑗)   𝐹(𝑖,𝑗)   𝐾(𝑖,𝑗)   𝐿(𝑖)   𝑉(𝑖,𝑗)   𝑍(𝑖,𝑗)

Proof of Theorem fedgmullem1

Dummy variables 𝑢 𝑘 𝑙 𝑔 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fedgmullem1.g	. . . . 5 ⊢ (𝜑 → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
2		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
3		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
4	2, 3	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5		elmapi 8799	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
6	4, 5	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
7	6	anasss 466	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
8		simprr 772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → 𝑖 ∈ 𝑋)
9	7, 8	ffvelcdmd 7039	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
10		fedgmul.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐸 ↾s 𝑉)
11		fedgmul.a	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)
12	11	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝐸)‘𝑉))
13		fedgmul.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))
14		fedgmul.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))
15		fedgmul.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝐸 ↾s 𝑈)
16	15	subsubrg 20518	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
17	16	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
18	13, 14, 17	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
19	18	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
20		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
21	20	subrgss 20492	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
22	19, 21	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
23	12, 22	srasca 21119	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
24	10, 23	eqtrid 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
25	18	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
26		ressabs 17194	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
27	13, 25, 26	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
28	15	oveq1i 7379	. . . . . . . . . . . . . 14 ⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉)
29	27, 28, 10	3eqtr4g 2789	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾)
30		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
31	30	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
32		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
33	32	subrgss 20492	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
34	14, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
35	31, 34	srasca 21119	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
36	29, 35	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
37	24, 36	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
38	37	fveq2d 6844	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
39	38	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
40	9, 39	eleqtrrd 2831	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
41	40	ralrimivva 3178	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
42		fedgmullem.h	. . . . . . . 8 ⊢ 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))
43	42	fmpo 8026	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
44	41, 43	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45		fvexd 6855	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (Base‘(Scalar‘𝐴)) ∈ V)
46		fedgmullem.y	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
47		fedgmullem.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
48	46, 47	xpexd 7707	. . . . . . . 8 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
49	48	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝑌 × 𝑋) ∈ V)
50	45, 49	elmapd 8790	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴))))
51	44, 50	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
52	1, 51	mpdan 687	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)))
53		simpl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝜑)
54	53	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝜑)
55	1	ffvelcdmda 7038	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
56	55, 5	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
57	56	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
58	38	feq3d 6655	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐴)) ↔ (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶))))
59	58	biimpar 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶))) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
60	54, 57, 59	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
61		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	60, 61	ffvelcdmd 7039	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
63	62	ralrimiva 3125	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
64	63	ralrimiva 3125	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
65	64, 43	sylib 218	. . . . 5 ⊢ (𝜑 → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
66	65	ffund 6674	. . . 4 ⊢ (𝜑 → Fun 𝐻)
67		fedgmul.1	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ DivRing)
68		drngring 20656	. . . . . 6 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
69	67, 68	syl 17	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Ring)
70		ringgrp 20158	. . . . 5 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71		eqid 2729	. . . . . 6 ⊢ (0g‘𝐸) = (0g‘𝐸)
72	20, 71	grpidcl 18879	. . . . 5 ⊢ (𝐸 ∈ Grp → (0g‘𝐸) ∈ (Base‘𝐸))
73	69, 70, 72	3syl 18	. . . 4 ⊢ (𝜑 → (0g‘𝐸) ∈ (Base‘𝐸))
74		fedgmullem1.1	. . . . . . 7 ⊢ (𝜑 → 𝐿 finSupp (0g‘(Scalar‘𝐵)))
75	74	fsuppimpd 9296	. . . . . 6 ⊢ (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ∈ Fin)
76		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝜑)
77		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵)))))
78	77	eldifad 3923	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ 𝑌)
79		fedgmullem1.l	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
80		ssidd 3967	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
81		fvexd 6855	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
82	79, 80, 46, 81	suppssr 8151	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿‘𝑗) = (0g‘(Scalar‘𝐵)))
83		fedgmullem1.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
84	78, 83	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
85		fedgmul.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
86	85	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
87	20	subrgss 20492	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
88	13, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
89	86, 88	srasca 21119	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
90	15, 89	eqtrid 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
91	90	fveq2d 6844	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐵)))
92		fedgmul.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ DivRing)
93	30, 92, 14	drgext0g 33578	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐹) = (0g‘𝐶))
94	91, 93	eqtr3d 2766	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
95	94	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
96	82, 84, 95	3eqtr3d 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶))
97		fedgmullem1.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)))
98		breq1 5105	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑔 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶))))
99		fveq1 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑔‘𝑖) = ((𝐺‘𝑗)‘𝑖))
100	99	oveq1d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
101	100	mpteq2dv 5196	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
102	101	oveq2d 7385	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝐺‘𝑗) → (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
103	102	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶) ↔ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)))
104	98, 103	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) ↔ ((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶))))
105		eqeq1 2733	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}) ↔ (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
106	104, 105	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑗) → (((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})) ↔ (((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
107		fedgmul.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ DivRing)
108	29, 107	eqeltrd 2828	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing)
109		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉)
110	30, 109	sralvec 33574	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
111	92, 108, 14, 110	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
112		lveclmod 21045	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
113	111, 112	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
114	113	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐶 ∈ LMod)
115		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐶) = (Base‘𝐶)
116		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
117	115, 116	lbsss 21016	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
118	47, 117	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
119	118	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ⊆ (Base‘𝐶))
120		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
121	115, 116, 120	islbs4 21774	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ (LBasis‘𝐶) ↔ (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
122	47, 121	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∈ (LIndS‘𝐶) ∧ ((LSpan‘𝐶)‘𝑋) = (Base‘𝐶)))
123	122	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ (LIndS‘𝐶))
124	123	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LIndS‘𝐶))
125		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
126		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
127		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘𝐶)
128		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (0g‘𝐶) = (0g‘𝐶)
129		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
130	115, 125, 126, 127, 128, 129	islinds5 33331	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) → (𝑋 ∈ (LIndS‘𝐶) ↔ ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))}))))
131	130	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ LMod ∧ 𝑋 ⊆ (Base‘𝐶)) ∧ 𝑋 ∈ (LIndS‘𝐶)) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
132	114, 119, 124, 131	syl21anc 837	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
133	106, 132, 55	rspcdva 3586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
134	97, 133	mpand 695	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
135	134	imp 406	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
136	76, 78, 96, 135	syl21anc 837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
137	1, 136	suppss 8150	. . . . . 6 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
138	75, 137	ssfid 9188	. . . . 5 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139		suppssdm 8133	. . . . . . . . . 10 ⊢ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140	139, 1	fssdm 6689	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141	140	sselda 3943	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤 ∈ 𝑌)
142		eleq1w 2811	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑤 → (𝑗 ∈ 𝑌 ↔ 𝑤 ∈ 𝑌))
143	142	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑤 → ((𝜑 ∧ 𝑗 ∈ 𝑌) ↔ (𝜑 ∧ 𝑤 ∈ 𝑌)))
144		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑤 → (𝐺‘𝑗) = (𝐺‘𝑤))
145	144	breq1d 5112	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑤 → ((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺‘𝑤) finSupp (0g‘(Scalar‘𝐶))))
146	143, 145	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑗 = 𝑤 → (((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝐺‘𝑤) finSupp (0g‘(Scalar‘𝐶)))))
147	146, 97	chvarvv 1989	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝐺‘𝑤) finSupp (0g‘(Scalar‘𝐶)))
148	147	fsuppimpd 9296	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
149	141, 148	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → ((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
150	149	ralrimiva 3125	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
151		iunfi 9270	. . . . . 6 ⊢ (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
152	138, 150, 151	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
153		xpfi 9245	. . . . 5 ⊢ (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
154	138, 152, 153	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
155		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑣 = 𝑗 → (𝐺‘𝑣) = (𝐺‘𝑗))
156	155	fveq1d 6842	. . . . . . . . 9 ⊢ (𝑣 = 𝑗 → ((𝐺‘𝑣)‘𝑢) = ((𝐺‘𝑗)‘𝑢))
157	156	mpteq2dv 5196	. . . . . . . 8 ⊢ (𝑣 = 𝑗 → (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)) = (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑢)))
158		fveq2 6840	. . . . . . . . 9 ⊢ (𝑢 = 𝑖 → ((𝐺‘𝑗)‘𝑢) = ((𝐺‘𝑗)‘𝑖))
159	158	cbvmptv 5206	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑢)) = (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))
160	157, 159	eqtrdi 2780	. . . . . . 7 ⊢ (𝑣 = 𝑗 → (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)) = (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
161	160	cbvmptv 5206	. . . . . 6 ⊢ (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) = (𝑗 ∈ 𝑌 ↦ (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
162		fvexd 6855	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163		fvexd 6855	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → ((𝐺‘𝑗)‘𝑖) ∈ V)
164	42, 161, 46, 47, 162, 163	suppovss 32654	. . . . 5 ⊢ (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
165	10, 71	subrg0 20499	. . . . . . . 8 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0g‘𝐸) = (0g‘𝐾))
166	19, 165	syl 17	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾))
167	36	fveq2d 6844	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐾) = (0g‘(Scalar‘𝐶)))
168	166, 167	eqtr2d 2765	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘𝐸))
169	168	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g‘𝐸)))
170	1	feqmptd 6911	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝑌 ↦ (𝐺‘𝑣)))
171		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑣 → (𝑗 ∈ 𝑌 ↔ 𝑣 ∈ 𝑌))
172	171	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑣 → ((𝜑 ∧ 𝑗 ∈ 𝑌) ↔ (𝜑 ∧ 𝑣 ∈ 𝑌)))
173		fveq2 6840	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑣 → (𝐺‘𝑗) = (𝐺‘𝑣))
174	173	feq1d 6652	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑣 → ((𝐺‘𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺‘𝑣):𝑋⟶(Base‘𝐸)))
175	172, 174	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑣 → (((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣):𝑋⟶(Base‘𝐸))))
176	10, 20	ressbas2 17184	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
177	22, 176	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
178	36	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
179	177, 178	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
180	179, 22	eqsstrrd 3979	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
181	180	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
182	56, 181	fssd 6687	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘𝐸))
183	175, 182	chvarvv 1989	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣):𝑋⟶(Base‘𝐸))
184	183	feqmptd 6911	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣) = (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))
185	184	mpteq2dva 5195	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝑌 ↦ (𝐺‘𝑣)) = (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))))
186	170, 185	eqtr2d 2765	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) = 𝐺)
187	186	oveq1d 7384	. . . . . 6 ⊢ (𝜑 → ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188	186	fveq1d 6842	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) = (𝐺‘𝑤))
189	188	oveq1d 7384	. . . . . . 7 ⊢ (𝜑 → (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))))
190	187, 189	iuneq12d 4981	. . . . . 6 ⊢ (𝜑 → ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))))
191	187, 190	xpeq12d 5662	. . . . 5 ⊢ (𝜑 → (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))) = ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))))
192	164, 169, 191	3sstr3d 3998	. . . 4 ⊢ (𝜑 → (𝐻 supp (0g‘𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))))
193		suppssfifsupp 9307	. . . 4 ⊢ (((𝐻 ∈ ((Base‘(Scalar‘𝐴)) ↑m (𝑌 × 𝑋)) ∧ Fun 𝐻 ∧ (0g‘𝐸) ∈ (Base‘𝐸)) ∧ (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin ∧ (𝐻 supp (0g‘𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))))) → 𝐻 finSupp (0g‘𝐸))
194	52, 66, 73, 154, 192, 193	syl32anc 1380	. . 3 ⊢ (𝜑 → 𝐻 finSupp (0g‘𝐸))
195	37	fveq2d 6844	. . . 4 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
196	195, 168	eqtr2d 2765	. . 3 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(Scalar‘𝐴)))
197	194, 196	breqtrd 5128	. 2 ⊢ (𝜑 → 𝐻 finSupp (0g‘(Scalar‘𝐴)))
198		fedgmullem1.z	. . 3 ⊢ (𝜑 → 𝑍 = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
199	85, 67, 13, 15, 92, 46	drgextgsum 33583	. . 3 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
200	47	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
201	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202		subrgsubg 20497	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203		subgsubm 19062	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204	201, 202, 203	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205	113	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
206	56	ffvelcdmda 7038	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207	118	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
208	207, 61	sseldd 3944	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
209	115, 126, 127, 125	lmodvscl 20816	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ LMod ∧ ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
210	205, 206, 208, 209	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
211	15, 20	ressbas2 17184	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
212	88, 211	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
213	31, 34	srabase 21116	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
214	212, 213	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
215	214	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
216	210, 215	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ 𝑈)
217	216	fmpttd 7069	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)):𝑋⟶𝑈)
218	200, 204, 217, 15	gsumsubm 18744	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
219		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐸) = (.r‘𝐸)
220	15, 219	ressmulr 17246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (.r‘𝐸) = (.r‘𝐹))
221	13, 220	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹))
222	31, 34	sravsca 21120	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝐹) = ( ·𝑠 ‘𝐶))
223	221, 222	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ( ·𝑠 ‘𝐶) = (.r‘𝐸))
224	223	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·𝑠 ‘𝐶) = (.r‘𝐸))
225	224	oveqd 7386	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))
226	225	mpteq2dva 5195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))
227	226	oveq2d 7385	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))))
228	30, 92, 14, 109, 108, 47	drgextgsum 33583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
229	228	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
230	218, 227, 229	3eqtr3d 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
231	230	oveq1d 7384	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))(.r‘𝐸)𝑗))
232	69	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
233	180	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
234	233, 206	sseldd 3944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘𝐸))
235	214, 88	eqsstrrd 3979	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
236	118, 235	sstrd 3954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
237	236	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐸))
238	237, 61	sseldd 3944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
239		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
240		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
241	239, 240	lbsss 21016	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
242	46, 241	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
243	86, 88	srabase 21116	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
244	242, 243	sseqtrrd 3981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
245	244	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑌 ⊆ (Base‘𝐸))
246		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
247	245, 246	sseldd 3944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
248	20, 219	ringass 20173	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Ring ∧ (((𝐺‘𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
249	232, 234, 238, 247, 248	syl13anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
250	249	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
251	250	oveq2d 7385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))))
252	69	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐸 ∈ Ring)
253	242	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ⊆ (Base‘𝐵))
254	243	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘𝐸) = (Base‘𝐵))
255	253, 254	sseqtrrd 3981	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ⊆ (Base‘𝐸))
256		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
257	255, 256	sseldd 3944	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
258	20, 219	ringcl 20170	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Ring ∧ ((𝐺‘𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
259	232, 234, 238, 258	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
260	168	breq2d 5114	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺‘𝑗) finSupp (0g‘𝐸)))
261	260	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺‘𝑗) finSupp (0g‘𝐸)))
262	97, 261	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘𝐸))
263	20, 252, 200, 238, 182, 262	rmfsupp2 33205	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸))
264	20, 71, 219, 252, 200, 257, 259, 263	gsummulc1 20236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
265	251, 264	eqtr3d 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
266	83	oveq1d 7384	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))(.r‘𝐸)𝑗))
267	231, 265, 266	3eqtr4rd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))))
268	86, 88	sravsca 21120	. . . . . . . . . 10 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
269	268	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
270	269	oveqd 7386	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))
271		fvexd 6855	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ V)
272		ovexd 7404	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ V)
273	42	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
274		fedgmullem.d	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))
275	274	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)))
276	46, 47, 271, 272, 273, 275	offval22 8044	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
277	276	oveqd 7386	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖))
278	277	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖))
279		ovexd 7404	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) ∈ V)
280		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
281	280	ovmpt4g 7516	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
282	246, 61, 279, 281	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
283	278, 282	eqtr2d 2765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) = (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))
284	283	mpteq2dva 5195	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) = (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖)))
285	284	oveq2d 7385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))
286	267, 270, 285	3eqtr3d 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))
287	286	mpteq2dva 5195	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖)))))
288	287	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))))
289		ringcmn 20202	. . . . . . 7 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ CMnd)
290	69, 289	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ CMnd)
291	69	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝐸 ∈ Ring)
292	38, 180	eqsstrd 3978	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
293	292	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
294		simprl 770	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘(Scalar‘𝐴)))
295	293, 294	sseldd 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘𝐸))
296		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐴))
297	12, 22	srabase 21116	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
298	297	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘𝐸) = (Base‘𝐴))
299	296, 298	eleqtrrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐸))
300	20, 219	ringcl 20170	. . . . . . . 8 ⊢ ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r‘𝐸)𝑘) ∈ (Base‘𝐸))
301	291, 295, 299, 300	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r‘𝐸)𝑘) ∈ (Base‘𝐸))
302	20, 219	ringcl 20170	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
303	232, 238, 247, 302	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
304	297	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
305	303, 304	eleqtrd 2830	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
306	305	anasss 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
307	306	ralrimivva 3178	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
308	274	fmpo 8026	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
309	307, 308	sylib 218	. . . . . . 7 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310		inidm 4186	. . . . . . 7 ⊢ ((𝑌 × 𝑋) ∩ (𝑌 × 𝑋)) = (𝑌 × 𝑋)
311	301, 65, 309, 48, 48, 310	off 7651	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷):(𝑌 × 𝑋)⟶(Base‘𝐸))
312	69	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → 𝐸 ∈ Ring)
313		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐴))
314	297	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → (Base‘𝐸) = (Base‘𝐴))
315	313, 314	eleqtrrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐸))
316	20, 219, 71	ringlz 20213	. . . . . . . 8 ⊢ ((𝐸 ∈ Ring ∧ 𝑢 ∈ (Base‘𝐸)) → ((0g‘𝐸)(.r‘𝐸)𝑢) = (0g‘𝐸))
317	312, 315, 316	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → ((0g‘𝐸)(.r‘𝐸)𝑢) = (0g‘𝐸))
318	48, 73, 73, 65, 309, 194, 317	offinsupp1 32700	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) finSupp (0g‘𝐸))
319	20, 71, 290, 46, 47, 311, 318	gsumxp 19890	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f (.r‘𝐸)𝐷)) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))))
320	12, 22	sravsca 21120	. . . . . . . 8 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
321	320	ofeqd 7635	. . . . . . 7 ⊢ (𝜑 → ∘f (.r‘𝐸) = ∘f ( ·𝑠 ‘𝐴))
322	321	oveqd 7386	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) = (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷))
323	322	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f (.r‘𝐸)𝐷)) = (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
324	288, 319, 323	3eqtr2rd 2771	. . . 4 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
325		ovexd 7404	. . . . 5 ⊢ (𝜑 → (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷) ∈ V)
326		fedgmullem1.a	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴))
327	326	elfvexd 6879	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
328	11, 325, 67, 327, 22	gsumsra 33030	. . . 4 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
329	324, 328	eqtr3d 2766	. . 3 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
330	198, 199, 329	3eqtr2d 2770	. 2 ⊢ (𝜑 → 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
331	197, 330	jca 511	1 ⊢ (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3444   ∖ cdif 3908   ⊆ wss 3911  {csn 4585  ∪ ciun 4951   class class class wbr 5102   ↦ cmpt 5183   × cxp 5629  Fun wfun 6493  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ∈ cmpo 7371   ∘_f cof 7631   supp csupp 8116   ↑_m cmap 8776  Fincfn 8895   finSupp cfsupp 9288  Basecbs 17155   ↾_s cress 17176  ._rcmulr 17197  Scalarcsca 17199   ·_𝑠 cvsca 17200  0_gc0g 17378   Σ_g cgsu 17379  SubMndcsubmnd 18691  Grpcgrp 18847  SubGrpcsubg 19034  CMndccmn 19694  Ringcrg 20153  SubRingcsubrg 20489  DivRingcdr 20649  LModclmod 20798  LSpanclspn 20909  LBasisclbs 21013  LVecclvec 21041  subringAlg csra 21110  LIndSclinds 21747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-sup 9369  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-fz 13445  df-fzo 13592  df-seq 13943  df-hash 14272  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-hom 17220  df-cco 17221  df-0g 17380  df-gsum 17381  df-prds 17386  df-pws 17388  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-mhm 18692  df-submnd 18693  df-grp 18850  df-minusg 18851  df-sbg 18852  df-mulg 18982  df-subg 19037  df-ghm 19127  df-cntz 19231  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-ring 20155  df-nzr 20433  df-subrg 20490  df-drng 20651  df-lmod 20800  df-lss 20870  df-lsp 20910  df-lmhm 20961  df-lbs 21014  df-lvec 21042  df-sra 21112  df-rgmod 21113  df-dsmm 21674  df-frlm 21689  df-uvc 21725  df-lindf 21748  df-linds 21749

This theorem is referenced by:  fedgmul  33620