Theorem fedgmullem1 33775

Description: Lemma for fedgmul 33777. (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 776	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))
3		simplr 769	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
4	2, 3	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5		elmapi 8798	. . . . . . . . . . . 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 773	. . . . . . . . . 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 20577	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (𝑉 ∈ (SubRing‘𝐹) ↔ (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈)))
17	16	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ∈ (SubRing‘𝐹)) → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
18	13, 14, 17	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈))
19	18	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐸))
20		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐸) = (Base‘𝐸)
21	20	subrgss 20551	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
22	19, 21	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
23	12, 22	srasca 21177	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
24	10, 23	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
25	18	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
26		ressabs 17220	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
27	13, 25, 26	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
28	15	oveq1i 7379	. . . . . . . . . . . . . 14 ⊢ (𝐹 ↾s 𝑉) = ((𝐸 ↾s 𝑈) ↾s 𝑉)
29	27, 28, 10	3eqtr4g 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = 𝐾)
30		fedgmul.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)
31	30	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 = ((subringAlg ‘𝐹)‘𝑉))
32		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐹) = (Base‘𝐹)
33	32	subrgss 20551	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
34	14, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
35	31, 34	srasca 21177	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
36	29, 35	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
37	24, 36	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
38	37	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
39	38	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐶)))
40	9, 39	eleqtrrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
41	40	ralrimivva 3181	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
42		fedgmullem.h	. . . . . . . 8 ⊢ 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))
43	42	fmpo 8023	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
44	41, 43	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45		fvexd 6857	. . . . . . 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 8789	. . . . . 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 688	. . . 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 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐴)))
61		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	60, 61	ffvelcdmd 7039	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
63	62	ralrimiva 3130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
64	63	ralrimiva 3130	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)))
65	64, 43	sylib 218	. . . . 5 ⊢ (𝜑 → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
66	65	ffund 6674	. . . 4 ⊢ (𝜑 → Fun 𝐻)
67		fedgmul.1	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ DivRing)
68		drngring 20715	. . . . . 6 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
69	67, 68	syl 17	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Ring)
70		ringgrp 20221	. . . . 5 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71		eqid 2737	. . . . . 6 ⊢ (0g‘𝐸) = (0g‘𝐸)
72	20, 71	grpidcl 18943	. . . . 5 ⊢ (𝐸 ∈ Grp → (0g‘𝐸) ∈ (Base‘𝐸))
73	69, 70, 72	3syl 18	. . . 4 ⊢ (𝜑 → (0g‘𝐸) ∈ (Base‘𝐸))
74		fedgmullem1.1	. . . . . . 7 ⊢ (𝜑 → 𝐿 finSupp (0g‘(Scalar‘𝐵)))
75	74	fsuppimpd 9284	. . . . . 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 3902	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → 𝑗 ∈ 𝑌)
79		fedgmullem1.l	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))
80		ssidd 3946	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 supp (0g‘(Scalar‘𝐵))) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
81		fvexd 6857	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
82	79, 80, 46, 81	suppssr 8147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿‘𝑗) = (0g‘(Scalar‘𝐵)))
83		fedgmullem1.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
84	78, 83	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
85		fedgmul.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
86	85	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈))
87	20	subrgss 20551	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
88	13, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
89	86, 88	srasca 21177	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
90	15, 89	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
91	90	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐵)))
92		fedgmul.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ DivRing)
93	30, 92, 14	drgext0g 33736	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐹) = (0g‘𝐶))
94	91, 93	eqtr3d 2774	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
95	94	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (0g‘(Scalar‘𝐵)) = (0g‘𝐶))
96	82, 84, 95	3eqtr3d 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶))
97		fedgmullem1.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)))
98		breq1 5089	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑔 finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶))))
99		fveq1 6841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑔‘𝑖) = ((𝐺‘𝑗)‘𝑖))
100	99	oveq1d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
101	100	mpteq2dv 5180	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
102	101	oveq2d 7385	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝐺‘𝑗) → (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
103	102	eqeq1d 2739	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶) ↔ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)))
104	98, 103	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) ↔ ((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶))))
105		eqeq1 2741	. . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾s 𝑉) ∈ DivRing)
109		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ↾s 𝑉) = (𝐹 ↾s 𝑉)
110	30, 109	sralvec 33731	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
111	92, 108, 14, 110	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
112		lveclmod 21103	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
113	111, 112	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ LMod)
114	113	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝐶 ∈ LMod)
115		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐶) = (Base‘𝐶)
116		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (LBasis‘𝐶) = (LBasis‘𝐶)
117	115, 116	lbsss 21074	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ (LBasis‘𝐶) → 𝑋 ⊆ (Base‘𝐶))
118	47, 117	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐶))
119	118	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ⊆ (Base‘𝐶))
120		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘𝐶) = (LSpan‘𝐶)
121	115, 116, 120	islbs4 21814	. . . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
126		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝐶) = (Scalar‘𝐶)
127		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝐶) = ( ·𝑠 ‘𝐶)
128		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (0g‘𝐶) = (0g‘𝐶)
129		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (0g‘(Scalar‘𝐶)) = (0g‘(Scalar‘𝐶))
130	115, 125, 126, 127, 128, 129	islinds5 33429	. . . . . . . . . . . . 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 838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ∀𝑔 ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋)((𝑔 finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → 𝑔 = (𝑋 × {(0g‘(Scalar‘𝐶))})))
133	106, 132, 55	rspcdva 3566	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
134	97, 133	mpand 696	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))})))
135	134	imp 406	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (0g‘𝐶)) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
136	76, 78, 96, 135	syl21anc 838	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑌 ∖ (𝐿 supp (0g‘(Scalar‘𝐵))))) → (𝐺‘𝑗) = (𝑋 × {(0g‘(Scalar‘𝐶))}))
137	1, 136	suppss 8146	. . . . . 6 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
138	75, 137	ssfid 9181	. . . . 5 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139		suppssdm 8129	. . . . . . . . . 10 ⊢ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140	139, 1	fssdm 6689	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141	140	sselda 3922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤 ∈ 𝑌)
142		eleq1w 2820	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑤 → (𝑗 ∈ 𝑌 ↔ 𝑤 ∈ 𝑌))
143	142	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑤 → ((𝜑 ∧ 𝑗 ∈ 𝑌) ↔ (𝜑 ∧ 𝑤 ∈ 𝑌)))
144		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑤 → (𝐺‘𝑗) = (𝐺‘𝑤))
145	144	breq1d 5096	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑤 → ((𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)) ↔ (𝐺‘𝑤) finSupp (0g‘(Scalar‘𝐶))))
146	143, 145	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑗 = 𝑤 → (((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝐺‘𝑤) finSupp (0g‘(Scalar‘𝐶)))))
147	146, 97	chvarvv 1991	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝐺‘𝑤) finSupp (0g‘(Scalar‘𝐶)))
148	147	fsuppimpd 9284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
149	141, 148	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → ((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
150	149	ralrimiva 3130	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
151		iunfi 9255	. . . . . 6 ⊢ (((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin ∧ ∀𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin) → ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
152	138, 150, 151	syl2anc 585	. . . . 5 ⊢ (𝜑 → ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))) ∈ Fin)
153		xpfi 9232	. . . . 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 585	. . . 4 ⊢ (𝜑 → ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))) ∈ Fin)
155		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑣 = 𝑗 → (𝐺‘𝑣) = (𝐺‘𝑗))
156	155	fveq1d 6844	. . . . . . . . 9 ⊢ (𝑣 = 𝑗 → ((𝐺‘𝑣)‘𝑢) = ((𝐺‘𝑗)‘𝑢))
157	156	mpteq2dv 5180	. . . . . . . 8 ⊢ (𝑣 = 𝑗 → (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)) = (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑢)))
158		fveq2 6842	. . . . . . . . 9 ⊢ (𝑢 = 𝑖 → ((𝐺‘𝑗)‘𝑢) = ((𝐺‘𝑗)‘𝑖))
159	158	cbvmptv 5190	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑢)) = (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))
160	157, 159	eqtrdi 2788	. . . . . . 7 ⊢ (𝑣 = 𝑗 → (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)) = (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
161	160	cbvmptv 5190	. . . . . 6 ⊢ (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) = (𝑗 ∈ 𝑌 ↦ (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
162		fvexd 6857	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163		fvexd 6857	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → ((𝐺‘𝑗)‘𝑖) ∈ V)
164	42, 161, 46, 47, 162, 163	suppovss 32756	. . . . 5 ⊢ (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
165	10, 71	subrg0 20558	. . . . . . . 8 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0g‘𝐸) = (0g‘𝐾))
166	19, 165	syl 17	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾))
167	36	fveq2d 6846	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐾) = (0g‘(Scalar‘𝐶)))
168	166, 167	eqtr2d 2773	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘𝐸))
169	168	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g‘𝐸)))
170	1	feqmptd 6910	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝑌 ↦ (𝐺‘𝑣)))
171		eleq1w 2820	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑣 → (𝑗 ∈ 𝑌 ↔ 𝑣 ∈ 𝑌))
172	171	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑣 → ((𝜑 ∧ 𝑗 ∈ 𝑌) ↔ (𝜑 ∧ 𝑣 ∈ 𝑌)))
173		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑣 → (𝐺‘𝑗) = (𝐺‘𝑣))
174	173	feq1d 6652	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑣 → ((𝐺‘𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺‘𝑣):𝑋⟶(Base‘𝐸)))
175	172, 174	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑣 → (((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣):𝑋⟶(Base‘𝐸))))
176	10, 20	ressbas2 17210	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
177	22, 176	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
178	36	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝐶)))
179	177, 178	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 = (Base‘(Scalar‘𝐶)))
180	179, 22	eqsstrrd 3958	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
181	180	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
182	56, 181	fssd 6687	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘𝐸))
183	175, 182	chvarvv 1991	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣):𝑋⟶(Base‘𝐸))
184	183	feqmptd 6910	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣) = (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))
185	184	mpteq2dva 5179	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝑌 ↦ (𝐺‘𝑣)) = (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))))
186	170, 185	eqtr2d 2773	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) = 𝐺)
187	186	oveq1d 7384	. . . . . 6 ⊢ (𝜑 → ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188	186	fveq1d 6844	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) = (𝐺‘𝑤))
189	188	oveq1d 7384	. . . . . . 7 ⊢ (𝜑 → (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))))
190	187, 189	iuneq12d 4964	. . . . . 6 ⊢ (𝜑 → ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶))) = ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶))))
191	187, 190	xpeq12d 5663	. . . . 5 ⊢ (𝜑 → (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))) = ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))))
192	164, 169, 191	3sstr3d 3977	. . . 4 ⊢ (𝜑 → (𝐻 supp (0g‘𝐸)) ⊆ ((𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))((𝐺‘𝑤) supp (0g‘(Scalar‘𝐶)))))
193		suppssfifsupp 9295	. . . 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 1381	. . 3 ⊢ (𝜑 → 𝐻 finSupp (0g‘𝐸))
195	37	fveq2d 6846	. . . 4 ⊢ (𝜑 → (0g‘(Scalar‘𝐴)) = (0g‘(Scalar‘𝐶)))
196	195, 168	eqtr2d 2773	. . 3 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(Scalar‘𝐴)))
197	194, 196	breqtrd 5112	. 2 ⊢ (𝜑 → 𝐻 finSupp (0g‘(Scalar‘𝐴)))
198		fedgmullem1.z	. . 3 ⊢ (𝜑 → 𝑍 = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
199	85, 67, 13, 15, 92, 46	drgextgsum 33741	. . 3 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
200	47	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
201	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202		subrgsubg 20556	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203		subgsubm 19126	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204	201, 202, 203	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205	113	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
206	56	ffvelcdmda 7038	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207	118	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
208	207, 61	sseldd 3923	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
209	115, 126, 127, 125	lmodvscl 20875	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ LMod ∧ ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
210	205, 206, 208, 209	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
211	15, 20	ressbas2 17210	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
212	88, 211	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
213	31, 34	srabase 21174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐹) = (Base‘𝐶))
214	212, 213	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
215	214	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑈 = (Base‘𝐶))
216	210, 215	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ 𝑈)
217	216	fmpttd 7069	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)):𝑋⟶𝑈)
218	200, 204, 217, 15	gsumsubm 18805	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
219		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐸) = (.r‘𝐸)
220	15, 219	ressmulr 17272	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (.r‘𝐸) = (.r‘𝐹))
221	13, 220	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹))
222	31, 34	sravsca 21178	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝐹) = ( ·𝑠 ‘𝐶))
223	221, 222	eqtr2d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ( ·𝑠 ‘𝐶) = (.r‘𝐸))
224	223	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·𝑠 ‘𝐶) = (.r‘𝐸))
225	224	oveqd 7386	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))
226	225	mpteq2dva 5179	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))
227	226	oveq2d 7385	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))))
228	30, 92, 14, 109, 108, 47	drgextgsum 33741	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
229	228	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
230	218, 227, 229	3eqtr3d 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
231	230	oveq1d 7384	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗) = ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))(.r‘𝐸)𝑗))
232	69	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ Ring)
233	180	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘(Scalar‘𝐶)) ⊆ (Base‘𝐸))
234	233, 206	sseldd 3923	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘𝐸))
235	214, 88	eqsstrrd 3958	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐶) ⊆ (Base‘𝐸))
236	118, 235	sstrd 3933	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝐸))
237	236	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐸))
238	237, 61	sseldd 3923	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐸))
239		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐵) = (Base‘𝐵)
240		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘𝐵) = (LBasis‘𝐵)
241	239, 240	lbsss 21074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
242	46, 241	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
243	86, 88	srabase 21174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵))
244	242, 243	sseqtrrd 3960	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐸))
245	244	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑌 ⊆ (Base‘𝐸))
246		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ 𝑌)
247	245, 246	sseldd 3923	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ (Base‘𝐸))
248	20, 219	ringass 20236	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Ring ∧ (((𝐺‘𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸))) → ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
249	232, 234, 238, 247, 248	syl13anc 1375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
250	249	mpteq2dva 5179	. . . . . . . . . . 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 3960	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑌 ⊆ (Base‘𝐸))
256		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ 𝑌)
257	255, 256	sseldd 3923	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ (Base‘𝐸))
258	20, 219	ringcl 20233	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Ring ∧ ((𝐺‘𝑗)‘𝑖) ∈ (Base‘𝐸) ∧ 𝑖 ∈ (Base‘𝐸)) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
259	232, 234, 238, 258	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖) ∈ (Base‘𝐸))
260	168	breq2d 5098	. . . . . . . . . . . . . 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 33301	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸))
264	20, 71, 219, 252, 200, 257, 259, 263	gsummulc1 20297	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
265	251, 264	eqtr3d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
266	83	oveq1d 7384	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))(.r‘𝐸)𝑗))
267	231, 265, 266	3eqtr4rd 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))))
268	86, 88	sravsca 21178	. . . . . . . . . 10 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
269	268	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
270	269	oveqd 7386	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))
271		fvexd 6857	. . . . . . . . . . . . . 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 8040	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
277	276	oveqd 7386	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖))
278	277	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖))
279		ovexd 7404	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) ∈ V)
280		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
281	280	ovmpt4g 7516	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋 ∧ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) ∈ V) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
282	246, 61, 279, 281	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
283	278, 282	eqtr2d 2773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) = (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))
284	283	mpteq2dva 5179	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) = (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖)))
285	284	oveq2d 7385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))
286	267, 270, 285	3eqtr3d 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))
287	286	mpteq2dva 5179	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗)) = (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖)))))
288	287	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))))
289		ringcmn 20265	. . . . . . 7 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ CMnd)
290	69, 289	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ CMnd)
291	69	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝐸 ∈ Ring)
292	38, 180	eqsstrd 3957	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
293	292	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) ⊆ (Base‘𝐸))
294		simprl 771	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘(Scalar‘𝐴)))
295	293, 294	sseldd 3923	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑙 ∈ (Base‘𝐸))
296		simprr 773	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐴))
297	12, 22	srabase 21174	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐴))
298	297	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (Base‘𝐸) = (Base‘𝐴))
299	296, 298	eleqtrrd 2840	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → 𝑘 ∈ (Base‘𝐸))
300	20, 219	ringcl 20233	. . . . . . . 8 ⊢ ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r‘𝐸)𝑘) ∈ (Base‘𝐸))
301	291, 295, 299, 300	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r‘𝐸)𝑘) ∈ (Base‘𝐸))
302	20, 219	ringcl 20233	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Ring ∧ 𝑖 ∈ (Base‘𝐸) ∧ 𝑗 ∈ (Base‘𝐸)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
303	232, 238, 247, 302	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐸))
304	297	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (Base‘𝐸) = (Base‘𝐴))
305	303, 304	eleqtrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
306	305	anasss 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
307	306	ralrimivva 3181	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴))
308	274	fmpo 8023	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
309	307, 308	sylib 218	. . . . . . 7 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310		inidm 4168	. . . . . . 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 2840	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → 𝑢 ∈ (Base‘𝐸))
316	20, 219, 71	ringlz 20276	. . . . . . . 8 ⊢ ((𝐸 ∈ Ring ∧ 𝑢 ∈ (Base‘𝐸)) → ((0g‘𝐸)(.r‘𝐸)𝑢) = (0g‘𝐸))
317	312, 315, 316	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (Base‘𝐴)) → ((0g‘𝐸)(.r‘𝐸)𝑢) = (0g‘𝐸))
318	48, 73, 73, 65, 309, 194, 317	offinsupp1 32801	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) finSupp (0g‘𝐸))
319	20, 71, 290, 46, 47, 311, 318	gsumxp 19953	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f (.r‘𝐸)𝐷)) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))))
320	12, 22	sravsca 21178	. . . . . . . 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 2779	. . . 4 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
325		ovexd 7404	. . . . 5 ⊢ (𝜑 → (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷) ∈ V)
326		fedgmullem1.a	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴))
327	326	elfvexd 6878	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
328	11, 325, 67, 327, 22	gsumsra 33110	. . . 4 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
329	324, 328	eqtr3d 2774	. . 3 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
330	198, 199, 329	3eqtr2d 2778	. 2 ⊢ (𝜑 → 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
331	197, 330	jca 511	1 ⊢ (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3430   ∖ cdif 3887   ⊆ wss 3890  {csn 4568  ∪ ciun 4934   class class class wbr 5086   ↦ cmpt 5167   × cxp 5630  Fun wfun 6494  ⟶wf 6496  ‘cfv 6500  (class class class)co 7369   ∈ cmpo 7371   ∘_f cof 7631   supp csupp 8112   ↑_m cmap 8775  Fincfn 8895   finSupp cfsupp 9276  Basecbs 17181   ↾_s cress 17202  ._rcmulr 17223  Scalarcsca 17225   ·_𝑠 cvsca 17226  0_gc0g 17404   Σ_g cgsu 17405  SubMndcsubmnd 18752  Grpcgrp 18911  SubGrpcsubg 19098  CMndccmn 19757  Ringcrg 20216  SubRingcsubrg 20548  DivRingcdr 20708  LModclmod 20857  LSpanclspn 20968  LBasisclbs 21071  LVecclvec 21099  subringAlg csra 21168  LIndSclinds 21787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7691  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7820  df-1st 7944  df-2nd 7945  df-supp 8113  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-sup 9357  df-oi 9427  df-card 9865  df-pnf 11183  df-mnf 11184  df-xr 11185  df-ltxr 11186  df-le 11187  df-sub 11381  df-neg 11382  df-nn 12177  df-2 12246  df-3 12247  df-4 12248  df-5 12249  df-6 12250  df-7 12251  df-8 12252  df-9 12253  df-n0 12440  df-z 12527  df-dec 12647  df-uz 12791  df-fz 13464  df-fzo 13611  df-seq 13966  df-hash 14295  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17182  df-ress 17203  df-plusg 17235  df-mulr 17236  df-sca 17238  df-vsca 17239  df-ip 17240  df-tset 17241  df-ple 17242  df-ds 17244  df-hom 17246  df-cco 17247  df-0g 17406  df-gsum 17407  df-prds 17412  df-pws 17414  df-mre 17550  df-mrc 17551  df-acs 17553  df-mgm 18610  df-sgrp 18689  df-mnd 18705  df-mhm 18753  df-submnd 18754  df-grp 18914  df-minusg 18915  df-sbg 18916  df-mulg 19046  df-subg 19101  df-ghm 19190  df-cntz 19294  df-cmn 19759  df-abl 19760  df-mgp 20124  df-rng 20136  df-ur 20165  df-ring 20218  df-nzr 20492  df-subrg 20549  df-drng 20710  df-lmod 20859  df-lss 20929  df-lsp 20969  df-lmhm 21019  df-lbs 21072  df-lvec 21100  df-sra 21170  df-rgmod 21171  df-dsmm 21714  df-frlm 21729  df-uvc 21765  df-lindf 21788  df-linds 21789

This theorem is referenced by:  fedgmul  33777