Theorem extdgfialglem1 33869

Description: Lemma for extdgfialg 33871. (Contributed by Thierry Arnoux, 10-Jan-2026.)

Hypotheses

Ref	Expression
extdgfialg.b	⊢ 𝐵 = (Base‘𝐸)
extdgfialg.d	⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))
extdgfialg.e	⊢ (𝜑 → 𝐸 ∈ Field)
extdgfialg.f	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
extdgfialg.1	⊢ (𝜑 → 𝐷 ∈ ℕ0)
extdgfialglem1.2	⊢ 𝑍 = (0g‘𝐸)
extdgfialglem1.3	⊢ · = (.r‘𝐸)
extdgfialglem1.r	⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
extdgfialglem1.4	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Assertion

Ref	Expression
extdgfialglem1	⊢ (𝜑 → ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))

Distinct variable groups:   · ,𝑛   𝐵,𝑛   𝐷,𝑛   𝑛,𝐸   𝑛,𝐹   𝑛,𝐺   𝑛,𝑋   𝑛,𝑍   𝜑,𝑛   𝐵,𝑎,𝑛   𝐷,𝑎   𝐸,𝑎   𝐹,𝑎   𝜑,𝑎   𝐺,𝑎   𝑋,𝑎

Allowed substitution hints:   · (𝑎)   𝑍(𝑎)

Proof of Theorem extdgfialglem1

Dummy variable 𝑏 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 769	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)))
2		extdgfialg.e	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐸 ∈ Field)
3	2	flddrngd 20686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ DivRing)
4		extdgfialg.f	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
5		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹)
6	5	sdrgdrng 20735	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing)
7	4, 6	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
8		sdrgsubrg 20736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
9	4, 8	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
10		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
11	10, 5	sralvec 33761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ DivRing ∧ (𝐸 ↾s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
12	3, 7, 9, 11	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
13	12	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
14	13	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
15		extdgfialg.d	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))
16		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) = (LBasis‘((subringAlg ‘𝐸)‘𝐹))
17	16	dimval 33777	. . . . . . . . . . . . . . . 16 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐹)) = (♯‘𝑏))
18	15, 17	eqtrid 2784	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 = (♯‘𝑏))
19	14, 1, 18	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝐷 = (♯‘𝑏))
20		extdgfialg.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℕ0)
21	20	ad4antr 733	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝐷 ∈ ℕ0)
22	19, 21	eqeltrrd 2838	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝑏) ∈ ℕ0)
23		hashclb 14293	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ0))
24	23	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ0) → 𝑏 ∈ Fin)
25	1, 22, 24	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝑏 ∈ Fin)
26		hashss 14344	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ Fin ∧ ran 𝐺 ⊆ 𝑏) → (♯‘ran 𝐺) ≤ (♯‘𝑏))
27	25, 26	sylancom 589	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘ran 𝐺) ≤ (♯‘𝑏))
28		extdgfialglem1.r	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
29	28	dmeqi 5861	. . . . . . . . . . . . . 14 ⊢ dom 𝐺 = dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
30		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
31		ovexd 7403	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
32	30, 31	dmmptd 6645	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) = (0...𝐷))
33		ovexd 7403	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (0...𝐷) ∈ V)
34	32, 33	eqeltrd 2837	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) ∈ V)
35	29, 34	eqeltrid 2841	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom 𝐺 ∈ V)
36		hashf1rn 14287	. . . . . . . . . . . . 13 ⊢ ((dom 𝐺 ∈ V ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘ran 𝐺))
37	35, 36	sylancom 589	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘ran 𝐺))
38	37	ad3antrrr 731	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝐺) = (♯‘ran 𝐺))
39	27, 38, 19	3brtr4d 5132	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝐺) ≤ 𝐷)
40	16	islinds4 21802	. . . . . . . . . . . 12 ⊢ (((subringAlg ‘𝐸)‘𝐹) ∈ LVec → (ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)) ↔ ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏))
41	40	biimpa 476	. . . . . . . . . . 11 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏)
42	13, 41	sylancom 589	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏)
43	39, 42	r19.29a 3146	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) ≤ 𝐷)
44	20	nn0red 12475	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℝ)
45	44	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 ∈ ℝ)
46	45	ltp1d 12084	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 < (𝐷 + 1))
47		fzfid 13908	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
48	47	mptexd 7180	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) ∈ V)
49	28, 48	eqeltrid 2841	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ V)
50	49	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → 𝐺 ∈ V)
51		f1f 6738	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:dom 𝐺–1-1→V → 𝐺:dom 𝐺⟶V)
52	51	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → 𝐺:dom 𝐺⟶V)
53	52	ffund 6674	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → Fun 𝐺)
54		hashfundm 14377	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ V ∧ Fun 𝐺) → (♯‘𝐺) = (♯‘dom 𝐺))
55	50, 53, 54	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘dom 𝐺))
56	28, 31	dmmptd 6645	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom 𝐺 = (0...𝐷))
57	56	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘dom 𝐺) = (♯‘(0...𝐷)))
58		hashfz0 14367	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ0 → (♯‘(0...𝐷)) = (𝐷 + 1))
59	20, 58	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(0...𝐷)) = (𝐷 + 1))
60	59	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘(0...𝐷)) = (𝐷 + 1))
61	55, 57, 60	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (𝐷 + 1))
62	61	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) = (𝐷 + 1))
63	46, 62	breqtrrd 5128	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 < (♯‘𝐺))
64	45	rexrd 11194	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 ∈ ℝ*)
65	50	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐺 ∈ V)
66		hashxrcl 14292	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ V → (♯‘𝐺) ∈ ℝ*)
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) ∈ ℝ*)
68	64, 67	xrltnled 11212	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (𝐷 < (♯‘𝐺) ↔ ¬ (♯‘𝐺) ≤ 𝐷))
69	63, 68	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ¬ (♯‘𝐺) ≤ 𝐷)
70	43, 69	pm2.65da 817	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → ¬ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))
71	70	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝐺:dom 𝐺–1-1→V → ¬ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))))
72		imnan 399	. . . . . . 7 ⊢ ((𝐺:dom 𝐺–1-1→V → ¬ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ↔ ¬ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))))
73	71, 72	sylib 218	. . . . . 6 ⊢ (𝜑 → ¬ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))))
74	12	lveclmodd 21071	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LMod)
75		eqidd 2738	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹))
76		extdgfialg.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐸)
77	76	sdrgss 20738	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
78	4, 77	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
79	78, 76	sseqtrdi 3976	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
80	75, 79	srasca 21144	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐸)‘𝐹)))
81		drngnzr 20693	. . . . . . . . 9 ⊢ ((𝐸 ↾s 𝐹) ∈ DivRing → (𝐸 ↾s 𝐹) ∈ NzRing)
82	7, 81	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ NzRing)
83	80, 82	eqeltrrd 2838	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ NzRing)
84		eqid 2737	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) = (Scalar‘((subringAlg ‘𝐸)‘𝐹))
85	84	islindf3 21793	. . . . . . 7 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ NzRing) → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))))
86	74, 83, 85	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))))
87	73, 86	mtbird 325	. . . . 5 ⊢ (𝜑 → ¬ 𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹))
88		ovexd 7403	. . . . . 6 ⊢ (𝜑 → (0...𝐷) ∈ V)
89		eqid 2737	. . . . . . . . 9 ⊢ (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) = (mulGrp‘((subringAlg ‘𝐸)‘𝐹))
90		eqid 2737	. . . . . . . . 9 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐹)) = (Base‘((subringAlg ‘𝐸)‘𝐹))
91	89, 90	mgpbas 20092	. . . . . . . 8 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐹)) = (Base‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))
92		eqid 2737	. . . . . . . 8 ⊢ (.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))) = (.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))
93	2	fldcrngd 20687	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ CRing)
94	93	crngringd 20193	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ Ring)
95	10, 76	sraring 21150	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ Ring ∧ 𝐹 ⊆ 𝐵) → ((subringAlg ‘𝐸)‘𝐹) ∈ Ring)
96	94, 78, 95	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ Ring)
97	89	ringmgp 20186	. . . . . . . . . 10 ⊢ (((subringAlg ‘𝐸)‘𝐹) ∈ Ring → (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) ∈ Mnd)
98	96, 97	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) ∈ Mnd)
99	98	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) ∈ Mnd)
100		fz0ssnn0 13550	. . . . . . . . . 10 ⊢ (0...𝐷) ⊆ ℕ0
101	100	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ0)
102	101	sselda 3935	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ0)
103		extdgfialglem1.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
104	75, 79	srabase 21141	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐹)))
105	76, 104	eqtr2id 2785	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐸)‘𝐹)) = 𝐵)
106	103, 105	eleqtrrd 2840	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
107	106	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
108	91, 92, 99, 102, 107	mulgnn0cld 19037	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
109	108, 28	fmptd 7068	. . . . . 6 ⊢ (𝜑 → 𝐺:(0...𝐷)⟶(Base‘((subringAlg ‘𝐸)‘𝐹)))
110		eqid 2737	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))
111		eqid 2737	. . . . . . 7 ⊢ (0g‘((subringAlg ‘𝐸)‘𝐹)) = (0g‘((subringAlg ‘𝐸)‘𝐹))
112		eqid 2737	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))
113		eqid 2737	. . . . . . 7 ⊢ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) = (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))
114	90, 84, 110, 111, 112, 113	islindf4 21805	. . . . . 6 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LMod ∧ (0...𝐷) ∈ V ∧ 𝐺:(0...𝐷)⟶(Base‘((subringAlg ‘𝐸)‘𝐹))) → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ ∀𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) → 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
115	74, 88, 109, 114	syl3anc 1374	. . . . 5 ⊢ (𝜑 → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ ∀𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) → 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
116	87, 115	mtbid 324	. . . 4 ⊢ (𝜑 → ¬ ∀𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) → 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
117		rexanali 3092	. . . 4 ⊢ (∃𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ¬ ∀𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) → 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
118	116, 117	sylibr 234	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
119		fvex 6855	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ V
120		ovex 7401	. . . . . . 7 ⊢ (0...𝐷) ∈ V
121		eqid 2737	. . . . . . . 8 ⊢ ((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)) = ((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))
122		eqid 2737	. . . . . . . 8 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))
123	121, 122, 112, 113	frlmelbas 21723	. . . . . . 7 ⊢ (((Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ V ∧ (0...𝐷) ∈ V) → (𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ↔ (𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ 𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))))
124	119, 120, 123	mp2an 693	. . . . . 6 ⊢ (𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ↔ (𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ 𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))))
125	124	anbi1i 625	. . . . 5 ⊢ ((𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ ((𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ 𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
126		df-ne 2934	. . . . . . 7 ⊢ (𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) ↔ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))
127	126	anbi2i 624	. . . . . 6 ⊢ (((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
128	127	anbi2i 624	. . . . 5 ⊢ ((𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ (𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
129		anass 468	. . . . 5 ⊢ (((𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ 𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ (𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))))
130	125, 128, 129	3bitr3i 301	. . . 4 ⊢ ((𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ (𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))))
131	130	rexbii2 3081	. . 3 ⊢ (∃𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷))(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
132	118, 131	sylib 218	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷))(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
133	5, 76	ressbas2 17177	. . . . . 6 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾s 𝐹)))
134	78, 133	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾s 𝐹)))
135	80	fveq2d 6846	. . . . 5 ⊢ (𝜑 → (Base‘(𝐸 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))
136	134, 135	eqtr2d 2773	. . . 4 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = 𝐹)
137	136	oveq1d 7383	. . 3 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) = (𝐹 ↑m (0...𝐷)))
138	93	crnggrpd 20194	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ Grp)
139	138	grpmndd 18888	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
140		subrgsubg 20522	. . . . . . . . . 10 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
141	9, 140	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
142		eqid 2737	. . . . . . . . . 10 ⊢ (0g‘𝐸) = (0g‘𝐸)
143	142	subg0cl 19076	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ 𝐹)
144	141, 143	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝐹)
145	5, 76, 142	ress0g 18699	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹)))
146	139, 144, 78, 145	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹)))
147	80	fveq2d 6846	. . . . . . 7 ⊢ (𝜑 → (0g‘(𝐸 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))
148	146, 147	eqtr2d 2773	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (0g‘𝐸))
149		extdgfialglem1.2	. . . . . 6 ⊢ 𝑍 = (0g‘𝐸)
150	148, 149	eqtr4di 2790	. . . . 5 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = 𝑍)
151	150	breq2d 5112	. . . 4 ⊢ (𝜑 → (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↔ 𝑎 finSupp 𝑍))
152		extdgfialglem1.3	. . . . . . . . . . 11 ⊢ · = (.r‘𝐸)
153	75, 79	sravsca 21145	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)))
154	152, 153	eqtr2id 2785	. . . . . . . . . 10 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = · )
155	154	ofeqd 7634	. . . . . . . . 9 ⊢ (𝜑 → ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = ∘f · )
156	155	oveqd 7385	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺) = (𝑎 ∘f · 𝐺))
157	156	oveq2d 7384	. . . . . . 7 ⊢ (𝜑 → (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f · 𝐺)))
158		ovexd 7403	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∘f · 𝐺) ∈ V)
159	10, 158, 2, 12, 79	gsumsra 33140	. . . . . . 7 ⊢ (𝜑 → (𝐸 Σg (𝑎 ∘f · 𝐺)) = (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f · 𝐺)))
160	157, 159	eqtr4d 2775	. . . . . 6 ⊢ (𝜑 → (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (𝐸 Σg (𝑎 ∘f · 𝐺)))
161	149	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑍 = (0g‘𝐸))
162	75, 161, 79	sralmod0 21152	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0g‘((subringAlg ‘𝐸)‘𝐹)))
163	162	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → (0g‘((subringAlg ‘𝐸)‘𝐹)) = 𝑍)
164	160, 163	eqeq12d 2753	. . . . 5 ⊢ (𝜑 → ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ↔ (𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍))
165	150	sneqd 4594	. . . . . . 7 ⊢ (𝜑 → {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))} = {𝑍})
166	165	xpeq2d 5662	. . . . . 6 ⊢ (𝜑 → ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) = ((0...𝐷) × {𝑍}))
167	166	neeq2d 2993	. . . . 5 ⊢ (𝜑 → (𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) ↔ 𝑎 ≠ ((0...𝐷) × {𝑍})))
168	164, 167	anbi12d 633	. . . 4 ⊢ (𝜑 → (((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))
169	151, 168	anbi12d 633	. . 3 ⊢ (𝜑 → ((𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ (𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍})))))
170	137, 169	rexeqbidv 3319	. 2 ⊢ (𝜑 → (∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷))(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍})))))
171	132, 170	mpbid 232	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3442   ⊆ wss 3903  {csn 4582   class class class wbr 5100   ↦ cmpt 5181   × cxp 5630  dom cdm 5632  ran crn 5633  Fun wfun 6494  ⟶wf 6496  –1-1→wf1 6497  ‘cfv 6500  (class class class)co 7368   ∘_f cof 7630   ↑_m cmap 8775  Fincfn 8895   finSupp cfsupp 9276  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041  ℝ^*cxr 11177   < clt 11178   ≤ cle 11179  ℕ₀cn0 12413  ...cfz 13435  ♯chash 14265  Basecbs 17148   ↾_s cress 17169  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  0_gc0g 17371   Σ_g cgsu 17372  Mndcmnd 18671  ._gcmg 19009  SubGrpcsubg 19062  mulGrpcmgp 20087  Ringcrg 20180  NzRingcnzr 20457  SubRingcsubrg 20514  DivRingcdr 20674  Fieldcfield 20675  SubDRingcsdrg 20731  LModclmod 20823  LBasisclbs 21038  LVecclvec 21066  subringAlg csra 21135   freeLMod cfrlm 21713   LIndF clindf 21771  LIndSclinds 21772  dimcldim 33775

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 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-reg 9509  ax-inf2 9562  ax-ac2 10385  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  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 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-rpss 7678  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-oadd 8411  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-r1 9688  df-rank 9689  df-dju 9825  df-card 9863  df-acn 9866  df-ac 10038  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-fz 13436  df-fzo 13583  df-seq 13937  df-hash 14266  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ocomp 17210  df-ds 17211  df-hom 17213  df-cco 17214  df-0g 17373  df-gsum 17374  df-prds 17379  df-pws 17381  df-mre 17517  df-mrc 17518  df-mri 17519  df-acs 17520  df-proset 18229  df-drs 18230  df-poset 18248  df-ipo 18463  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-grp 18878  df-minusg 18879  df-sbg 18880  df-mulg 19010  df-subg 19065  df-ghm 19154  df-cntz 19258  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-ring 20182  df-cring 20183  df-oppr 20285  df-dvdsr 20305  df-unit 20306  df-invr 20336  df-nzr 20458  df-subrg 20515  df-drng 20676  df-field 20677  df-sdrg 20732  df-lmod 20825  df-lss 20895  df-lsp 20935  df-lmhm 20986  df-lbs 21039  df-lvec 21067  df-sra 21137  df-rgmod 21138  df-dsmm 21699  df-frlm 21714  df-uvc 21750  df-lindf 21773  df-linds 21774  df-dim 33776

This theorem is referenced by:  extdgfialg  33871