Theorem fedgmullem1 33793

Description: Lemma for fedgmul 33795. (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 7033	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
5		elmapi 8791	. . . . . . . . . . . 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 7033	. . . . . . . . 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 20570	. . . . . . . . . . . . . . . . . 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 20544	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐸) → 𝑉 ⊆ (Base‘𝐸))
22	19, 21	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐸))
23	12, 22	srasca 21171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝑉) = (Scalar‘𝐴))
24	10, 23	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐴))
25	18	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ⊆ 𝑈)
26		ressabs 17213	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ (SubRing‘𝐸) ∧ 𝑉 ⊆ 𝑈) → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
27	13, 25, 26	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 ↾s 𝑈) ↾s 𝑉) = (𝐸 ↾s 𝑉))
28	15	oveq1i 7372	. . . . . . . . . . . . . 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 20544	. . . . . . . . . . . . . . 15 ⊢ (𝑉 ∈ (SubRing‘𝐹) → 𝑉 ⊆ (Base‘𝐹))
34	14, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐹))
35	31, 34	srasca 21171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾s 𝑉) = (Scalar‘𝐶))
36	29, 35	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = (Scalar‘𝐶))
37	24, 36	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → (Scalar‘𝐴) = (Scalar‘𝐶))
38	37	fveq2d 6840	. . . . . . . . . 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 8016	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐴)) ↔ 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
44	41, 43	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → 𝐻:(𝑌 × 𝑋)⟶(Base‘(Scalar‘𝐴)))
45		fvexd 6851	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (Base‘(Scalar‘𝐴)) ∈ V)
46		fedgmullem.y	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))
47		fedgmullem.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))
48	46, 47	xpexd 7700	. . . . . . . 8 ⊢ (𝜑 → (𝑌 × 𝑋) ∈ V)
49	48	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) → (𝑌 × 𝑋) ∈ V)
50	45, 49	elmapd 8782	. . . . . 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 7032	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) ∈ ((Base‘(Scalar‘𝐶)) ↑m 𝑋))
56	55, 5	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
57	56	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝐺‘𝑗):𝑋⟶(Base‘(Scalar‘𝐶)))
58	38	feq3d 6649	. . . . . . . . . . 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 7033	. . . . . . . 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 6668	. . . 4 ⊢ (𝜑 → Fun 𝐻)
67		fedgmul.1	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ DivRing)
68		drngring 20708	. . . . . 6 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
69	67, 68	syl 17	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Ring)
70		ringgrp 20214	. . . . 5 ⊢ (𝐸 ∈ Ring → 𝐸 ∈ Grp)
71		eqid 2737	. . . . . 6 ⊢ (0g‘𝐸) = (0g‘𝐸)
72	20, 71	grpidcl 18936	. . . . 5 ⊢ (𝐸 ∈ Grp → (0g‘𝐸) ∈ (Base‘𝐸))
73	69, 70, 72	3syl 18	. . . 4 ⊢ (𝜑 → (0g‘𝐸) ∈ (Base‘𝐸))
74		fedgmullem1.1	. . . . . . 7 ⊢ (𝜑 → 𝐿 finSupp (0g‘(Scalar‘𝐵)))
75	74	fsuppimpd 9277	. . . . . 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 6851	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(Scalar‘𝐵)) ∈ V)
82	79, 80, 46, 81	suppssr 8140	. . . . . . . . 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 20544	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
88	13, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸))
89	86, 88	srasca 21171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵))
90	15, 89	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = (Scalar‘𝐵))
91	90	fveq2d 6840	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐹) = (0g‘(Scalar‘𝐵)))
92		fedgmul.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ DivRing)
93	30, 92, 14	drgext0g 33753	. . . . . . . . . . 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 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑔‘𝑖) = ((𝐺‘𝑗)‘𝑖))
100	99	oveq1d 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝐺‘𝑗) → ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))
101	100	mpteq2dv 5180	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝐺‘𝑗) → (𝑖 ∈ 𝑋 ↦ ((𝑔‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))
102	101	oveq2d 7378	. . . . . . . . . . . . . 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 33748	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ DivRing ∧ (𝐹 ↾s 𝑉) ∈ DivRing ∧ 𝑉 ∈ (SubRing‘𝐹)) → 𝐶 ∈ LVec)
111	92, 108, 14, 110	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ LVec)
112		lveclmod 21097	. . . . . . . . . . . . . 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 21068	. . . . . . . . . . . . . 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 21826	. . . . . . . . . . . . . . 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 33446	. . . . . . . . . . . . 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 8139	. . . . . 6 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ (𝐿 supp (0g‘(Scalar‘𝐵))))
138	75, 137	ssfid 9174	. . . . 5 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ∈ Fin)
139		suppssdm 8122	. . . . . . . . . 10 ⊢ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ dom 𝐺
140	139, 1	fssdm 6683	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})) ⊆ 𝑌)
141	140	sselda 3922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))}))) → 𝑤 ∈ 𝑌)
142		eleq1w 2820	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑤 → (𝑗 ∈ 𝑌 ↔ 𝑤 ∈ 𝑌))
143	142	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑤 → ((𝜑 ∧ 𝑗 ∈ 𝑌) ↔ (𝜑 ∧ 𝑤 ∈ 𝑌)))
144		fveq2 6836	. . . . . . . . . . . 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 9277	. . . . . . . 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 9248	. . . . . 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 9225	. . . . 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 6836	. . . . . . . . . 10 ⊢ (𝑣 = 𝑗 → (𝐺‘𝑣) = (𝐺‘𝑗))
156	155	fveq1d 6838	. . . . . . . . 9 ⊢ (𝑣 = 𝑗 → ((𝐺‘𝑣)‘𝑢) = ((𝐺‘𝑗)‘𝑢))
157	156	mpteq2dv 5180	. . . . . . . 8 ⊢ (𝑣 = 𝑗 → (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)) = (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑢)))
158		fveq2 6836	. . . . . . . . 9 ⊢ (𝑢 = 𝑖 → ((𝐺‘𝑗)‘𝑢) = ((𝐺‘𝑗)‘𝑖))
159	158	cbvmptv 5190	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑢)) = (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))
160	157, 159	eqtrdi 2788	. . . . . . 7 ⊢ (𝑣 = 𝑗 → (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)) = (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
161	160	cbvmptv 5190	. . . . . 6 ⊢ (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) = (𝑗 ∈ 𝑌 ↦ (𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)))
162		fvexd 6851	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) ∈ V)
163		fvexd 6851	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋)) → ((𝐺‘𝑗)‘𝑖) ∈ V)
164	42, 161, 46, 47, 162, 163	suppovss 32773	. . . . 5 ⊢ (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) ⊆ (((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) × ∪ 𝑤 ∈ ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))}))(((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) supp (0g‘(Scalar‘𝐶)))))
165	10, 71	subrg0 20551	. . . . . . . 8 ⊢ (𝑉 ∈ (SubRing‘𝐸) → (0g‘𝐸) = (0g‘𝐾))
166	19, 165	syl 17	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐾))
167	36	fveq2d 6840	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐾) = (0g‘(Scalar‘𝐶)))
168	166, 167	eqtr2d 2773	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘𝐶)) = (0g‘𝐸))
169	168	oveq2d 7378	. . . . 5 ⊢ (𝜑 → (𝐻 supp (0g‘(Scalar‘𝐶))) = (𝐻 supp (0g‘𝐸)))
170	1	feqmptd 6904	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝑌 ↦ (𝐺‘𝑣)))
171		eleq1w 2820	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑣 → (𝑗 ∈ 𝑌 ↔ 𝑣 ∈ 𝑌))
172	171	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑣 → ((𝜑 ∧ 𝑗 ∈ 𝑌) ↔ (𝜑 ∧ 𝑣 ∈ 𝑌)))
173		fveq2 6836	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑣 → (𝐺‘𝑗) = (𝐺‘𝑣))
174	173	feq1d 6646	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑣 → ((𝐺‘𝑗):𝑋⟶(Base‘𝐸) ↔ (𝐺‘𝑣):𝑋⟶(Base‘𝐸)))
175	172, 174	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑣 → (((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘𝐸)) ↔ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣):𝑋⟶(Base‘𝐸))))
176	10, 20	ressbas2 17203	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ⊆ (Base‘𝐸) → 𝑉 = (Base‘𝐾))
177	22, 176	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 = (Base‘𝐾))
178	36	fveq2d 6840	. . . . . . . . . . . . . . 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 6681	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗):𝑋⟶(Base‘𝐸))
183	175, 182	chvarvv 1991	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣):𝑋⟶(Base‘𝐸))
184	183	feqmptd 6904	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑌) → (𝐺‘𝑣) = (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))
185	184	mpteq2dva 5179	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ 𝑌 ↦ (𝐺‘𝑣)) = (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))))
186	170, 185	eqtr2d 2773	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) = 𝐺)
187	186	oveq1d 7377	. . . . . 6 ⊢ (𝜑 → ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢))) supp (𝑋 × {(0g‘(Scalar‘𝐶))})) = (𝐺 supp (𝑋 × {(0g‘(Scalar‘𝐶))})))
188	186	fveq1d 6838	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝑌 ↦ (𝑢 ∈ 𝑋 ↦ ((𝐺‘𝑣)‘𝑢)))‘𝑤) = (𝐺‘𝑤))
189	188	oveq1d 7377	. . . . . . 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 5657	. . . . 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 9288	. . . 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 6840	. . . 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 33758	. . 3 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
200	47	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑋 ∈ (LBasis‘𝐶))
201	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubRing‘𝐸))
202		subrgsubg 20549	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
203		subgsubm 19119	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubGrp‘𝐸) → 𝑈 ∈ (SubMnd‘𝐸))
204	201, 202, 203	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → 𝑈 ∈ (SubMnd‘𝐸))
205	113	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝐶 ∈ LMod)
206	56	ffvelcdmda 7032	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)))
207	118	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑋 ⊆ (Base‘𝐶))
208	207, 61	sseldd 3923	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ (Base‘𝐶))
209	115, 126, 127, 125	lmodvscl 20868	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ LMod ∧ ((𝐺‘𝑗)‘𝑖) ∈ (Base‘(Scalar‘𝐶)) ∧ 𝑖 ∈ (Base‘𝐶)) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
210	205, 206, 208, 209	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) ∈ (Base‘𝐶))
211	15, 20	ressbas2 17203	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹))
212	88, 211	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝐹))
213	31, 34	srabase 21168	. . . . . . . . . . . . . . . 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 7063	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)):𝑋⟶𝑈)
218	200, 204, 217, 15	gsumsubm 18798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
219		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐸) = (.r‘𝐸)
220	15, 219	ressmulr 17265	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ (SubRing‘𝐸) → (.r‘𝐸) = (.r‘𝐹))
221	13, 220	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹))
222	31, 34	sravsca 21172	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝐹) = ( ·𝑠 ‘𝐶))
223	221, 222	eqtr2d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ( ·𝑠 ‘𝐶) = (.r‘𝐸))
224	223	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → ( ·𝑠 ‘𝐶) = (.r‘𝐸))
225	224	oveqd 7379	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖) = (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))
226	225	mpteq2dva 5179	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)) = (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))
227	226	oveq2d 7378	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))))
228	30, 92, 14, 109, 108, 47	drgextgsum 33758	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
229	228	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐹 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
230	218, 227, 229	3eqtr3d 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖))) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))
231	230	oveq1d 7377	. . . . . . . . 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 21068	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∈ (LBasis‘𝐵) → 𝑌 ⊆ (Base‘𝐵))
242	46, 241	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝐵))
243	86, 88	srabase 21168	. . . . . . . . . . . . . . . 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 20229	. . . . . . . . . . . . 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 7378	. . . . . . . . . 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 20226	. . . . . . . . . . . 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 33318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)) finSupp (0g‘𝐸))
264	20, 71, 219, 252, 200, 257, 259, 263	gsummulc1 20290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ ((((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)(.r‘𝐸)𝑗))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
265	251, 264	eqtr3d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))) = ((𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)𝑖)))(.r‘𝐸)𝑗))
266	83	oveq1d 7377	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = ((𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))(.r‘𝐸)𝑗))
267	231, 265, 266	3eqtr4rd 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))))
268	86, 88	sravsca 21172	. . . . . . . . . 10 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
269	268	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
270	269	oveqd 7379	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → ((𝐿‘𝑗)(.r‘𝐸)𝑗) = ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))
271		fvexd 6851	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌 ∧ 𝑖 ∈ 𝑋) → ((𝐺‘𝑗)‘𝑖) ∈ V)
272		ovexd 7397	. . . . . . . . . . . . . 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 8033	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))))
277	276	oveqd 7379	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖))
278	277	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖) = (𝑗(𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))𝑖))
279		ovexd 7397	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑌) ∧ 𝑖 ∈ 𝑋) → (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)) ∈ V)
280		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗))) = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)(.r‘𝐸)(𝑖(.r‘𝐸)𝑗)))
281	280	ovmpt4g 7509	. . . . . . . . . . . 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 7378	. . . . . . . 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 7378	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))))
289		ringcmn 20258	. . . . . . 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 21168	. . . . . . . . . 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 20226	. . . . . . . 8 ⊢ ((𝐸 ∈ Ring ∧ 𝑙 ∈ (Base‘𝐸) ∧ 𝑘 ∈ (Base‘𝐸)) → (𝑙(.r‘𝐸)𝑘) ∈ (Base‘𝐸))
301	291, 295, 299, 300	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑙 ∈ (Base‘(Scalar‘𝐴)) ∧ 𝑘 ∈ (Base‘𝐴))) → (𝑙(.r‘𝐸)𝑘) ∈ (Base‘𝐸))
302	20, 219	ringcl 20226	. . . . . . . . . . . 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 8016	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝑌 ∀𝑖 ∈ 𝑋 (𝑖(.r‘𝐸)𝑗) ∈ (Base‘𝐴) ↔ 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
309	307, 308	sylib 218	. . . . . . 7 ⊢ (𝜑 → 𝐷:(𝑌 × 𝑋)⟶(Base‘𝐴))
310		inidm 4168	. . . . . . 7 ⊢ ((𝑌 × 𝑋) ∩ (𝑌 × 𝑋)) = (𝑌 × 𝑋)
311	301, 65, 309, 48, 48, 310	off 7644	. . . . . 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 20269	. . . . . . . 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 32818	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) finSupp (0g‘𝐸))
319	20, 71, 290, 46, 47, 311, 318	gsumxp 19946	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f (.r‘𝐸)𝐷)) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ (𝐸 Σg (𝑖 ∈ 𝑋 ↦ (𝑗(𝐻 ∘f (.r‘𝐸)𝐷)𝑖))))))
320	12, 22	sravsca 21172	. . . . . . . 8 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐴))
321	320	ofeqd 7628	. . . . . . 7 ⊢ (𝜑 → ∘f (.r‘𝐸) = ∘f ( ·𝑠 ‘𝐴))
322	321	oveqd 7379	. . . . . 6 ⊢ (𝜑 → (𝐻 ∘f (.r‘𝐸)𝐷) = (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷))
323	322	oveq2d 7378	. . . . 5 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f (.r‘𝐸)𝐷)) = (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))
324	288, 319, 323	3eqtr2rd 2779	. . . 4 ⊢ (𝜑 → (𝐸 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (𝐸 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))
325		ovexd 7397	. . . . 5 ⊢ (𝜑 → (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷) ∈ V)
326		fedgmullem1.a	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴))
327	326	elfvexd 6872	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
328	11, 325, 67, 327, 22	gsumsra 33127	. . . 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 5624  Fun wfun 6488  ⟶wf 6490  ‘cfv 6494  (class class class)co 7362   ∈ cmpo 7364   ∘_f cof 7624   supp csupp 8105   ↑_m cmap 8768  Fincfn 8888   finSupp cfsupp 9269  Basecbs 17174   ↾_s cress 17195  ._rcmulr 17216  Scalarcsca 17218   ·_𝑠 cvsca 17219  0_gc0g 17397   Σ_g cgsu 17398  SubMndcsubmnd 18745  Grpcgrp 18904  SubGrpcsubg 19091  CMndccmn 19750  Ringcrg 20209  SubRingcsubrg 20541  DivRingcdr 20701  LModclmod 20850  LSpanclspn 20961  LBasisclbs 21065  LVecclvec 21093  subringAlg csra 21162  LIndSclinds 21799

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 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

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 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-se 5580  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-isom 6503  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7626  df-om 7813  df-1st 7937  df-2nd 7938  df-supp 8106  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-1o 8400  df-2o 8401  df-er 8638  df-map 8770  df-ixp 8841  df-en 8889  df-dom 8890  df-sdom 8891  df-fin 8892  df-fsupp 9270  df-sup 9350  df-oi 9420  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-fz 13457  df-fzo 13604  df-seq 13959  df-hash 14288  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-sca 17231  df-vsca 17232  df-ip 17233  df-tset 17234  df-ple 17235  df-ds 17237  df-hom 17239  df-cco 17240  df-0g 17399  df-gsum 17400  df-prds 17405  df-pws 17407  df-mre 17543  df-mrc 17544  df-acs 17546  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18746  df-submnd 18747  df-grp 18907  df-minusg 18908  df-sbg 18909  df-mulg 19039  df-subg 19094  df-ghm 19183  df-cntz 19287  df-cmn 19752  df-abl 19753  df-mgp 20117  df-rng 20129  df-ur 20158  df-ring 20211  df-nzr 20485  df-subrg 20542  df-drng 20703  df-lmod 20852  df-lss 20922  df-lsp 20962  df-lmhm 21013  df-lbs 21066  df-lvec 21094  df-sra 21164  df-rgmod 21165  df-dsmm 21726  df-frlm 21741  df-uvc 21777  df-lindf 21800  df-linds 21801

This theorem is referenced by:  fedgmul  33795