Theorem extdgfialglem1 33678

Description: Lemma for extdgfialg 33680. (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 768	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)))
2		extdgfialg.e	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐸 ∈ Field)
3	2	flddrngd 20645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ DivRing)
4		extdgfialg.f	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
5		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹)
6	5	sdrgdrng 20694	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing)
7	4, 6	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
8		sdrgsubrg 20695	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
9	4, 8	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
10		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
11	10, 5	sralvec 33570	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ DivRing ∧ (𝐸 ↾s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
12	3, 7, 9, 11	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
13	12	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
14	13	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
15		extdgfialg.d	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))
16		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) = (LBasis‘((subringAlg ‘𝐸)‘𝐹))
17	16	dimval 33586	. . . . . . . . . . . . . . . 16 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐹)) = (♯‘𝑏))
18	15, 17	eqtrid 2776	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 = (♯‘𝑏))
19	14, 1, 18	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝐷 = (♯‘𝑏))
20		extdgfialg.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℕ0)
21	20	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝐷 ∈ ℕ0)
22	19, 21	eqeltrrd 2829	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝑏) ∈ ℕ0)
23		hashclb 14284	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ0))
24	23	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ0) → 𝑏 ∈ Fin)
25	1, 22, 24	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝑏 ∈ Fin)
26		hashss 14335	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ Fin ∧ ran 𝐺 ⊆ 𝑏) → (♯‘ran 𝐺) ≤ (♯‘𝑏))
27	25, 26	sylancom 588	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘ran 𝐺) ≤ (♯‘𝑏))
28		extdgfialglem1.r	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
29	28	dmeqi 5851	. . . . . . . . . . . . . 14 ⊢ dom 𝐺 = dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
30		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
31		ovexd 7388	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
32	30, 31	dmmptd 6631	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) = (0...𝐷))
33		ovexd 7388	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (0...𝐷) ∈ V)
34	32, 33	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) ∈ V)
35	29, 34	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom 𝐺 ∈ V)
36		hashf1rn 14278	. . . . . . . . . . . . 13 ⊢ ((dom 𝐺 ∈ V ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘ran 𝐺))
37	35, 36	sylancom 588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘ran 𝐺))
38	37	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝐺) = (♯‘ran 𝐺))
39	27, 38, 19	3brtr4d 5127	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝐺) ≤ 𝐷)
40	16	islinds4 21761	. . . . . . . . . . . 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 588	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏)
43	39, 42	r19.29a 3137	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) ≤ 𝐷)
44	20	nn0red 12465	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℝ)
45	44	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 ∈ ℝ)
46	45	ltp1d 12074	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 < (𝐷 + 1))
47		fzfid 13899	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
48	47	mptexd 7164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) ∈ V)
49	28, 48	eqeltrid 2832	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ V)
50	49	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → 𝐺 ∈ V)
51		f1f 6724	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:dom 𝐺–1-1→V → 𝐺:dom 𝐺⟶V)
52	51	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → 𝐺:dom 𝐺⟶V)
53	52	ffund 6660	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → Fun 𝐺)
54		hashfundm 14368	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ V ∧ Fun 𝐺) → (♯‘𝐺) = (♯‘dom 𝐺))
55	50, 53, 54	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘dom 𝐺))
56	28, 31	dmmptd 6631	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom 𝐺 = (0...𝐷))
57	56	fveq2d 6830	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘dom 𝐺) = (♯‘(0...𝐷)))
58		hashfz0 14358	. . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (𝐷 + 1))
62	61	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) = (𝐷 + 1))
63	46, 62	breqtrrd 5123	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 < (♯‘𝐺))
64	45	rexrd 11184	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 ∈ ℝ*)
65	50	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐺 ∈ V)
66		hashxrcl 14283	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ V → (♯‘𝐺) ∈ ℝ*)
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) ∈ ℝ*)
68	64, 67	xrltnled 11202	. . . . . . . . . 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 816	. . . . . . . 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 21030	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LMod)
75		eqidd 2730	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹))
76		extdgfialg.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐸)
77	76	sdrgss 20697	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
78	4, 77	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
79	78, 76	sseqtrdi 3978	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
80	75, 79	srasca 21103	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐸)‘𝐹)))
81		drngnzr 20652	. . . . . . . . 9 ⊢ ((𝐸 ↾s 𝐹) ∈ DivRing → (𝐸 ↾s 𝐹) ∈ NzRing)
82	7, 81	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ NzRing)
83	80, 82	eqeltrrd 2829	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ NzRing)
84		eqid 2729	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) = (Scalar‘((subringAlg ‘𝐸)‘𝐹))
85	84	islindf3 21752	. . . . . . 7 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ NzRing) → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))))
86	74, 83, 85	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))))
87	73, 86	mtbird 325	. . . . 5 ⊢ (𝜑 → ¬ 𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹))
88		ovexd 7388	. . . . . 6 ⊢ (𝜑 → (0...𝐷) ∈ V)
89		eqid 2729	. . . . . . . . 9 ⊢ (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) = (mulGrp‘((subringAlg ‘𝐸)‘𝐹))
90		eqid 2729	. . . . . . . . 9 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐹)) = (Base‘((subringAlg ‘𝐸)‘𝐹))
91	89, 90	mgpbas 20049	. . . . . . . 8 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐹)) = (Base‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))
92		eqid 2729	. . . . . . . 8 ⊢ (.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))) = (.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))
93	2	fldcrngd 20646	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ CRing)
94	93	crngringd 20150	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ Ring)
95	10, 76	sraring 21109	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ Ring ∧ 𝐹 ⊆ 𝐵) → ((subringAlg ‘𝐸)‘𝐹) ∈ Ring)
96	94, 78, 95	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ Ring)
97	89	ringmgp 20143	. . . . . . . . . 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 13544	. . . . . . . . . 10 ⊢ (0...𝐷) ⊆ ℕ0
101	100	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ0)
102	101	sselda 3937	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ0)
103		extdgfialglem1.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
104	75, 79	srabase 21100	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐹)))
105	76, 104	eqtr2id 2777	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐸)‘𝐹)) = 𝐵)
106	103, 105	eleqtrrd 2831	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
107	106	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
108	91, 92, 99, 102, 107	mulgnn0cld 18993	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
109	108, 28	fmptd 7052	. . . . . 6 ⊢ (𝜑 → 𝐺:(0...𝐷)⟶(Base‘((subringAlg ‘𝐸)‘𝐹)))
110		eqid 2729	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))
111		eqid 2729	. . . . . . 7 ⊢ (0g‘((subringAlg ‘𝐸)‘𝐹)) = (0g‘((subringAlg ‘𝐸)‘𝐹))
112		eqid 2729	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))
113		eqid 2729	. . . . . . 7 ⊢ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) = (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))
114	90, 84, 110, 111, 112, 113	islindf4 21764	. . . . . 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 1373	. . . . 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 3083	. . . 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 6839	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ V
120		ovex 7386	. . . . . . 7 ⊢ (0...𝐷) ∈ V
121		eqid 2729	. . . . . . . 8 ⊢ ((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)) = ((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))
122		eqid 2729	. . . . . . . 8 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))
123	121, 122, 112, 113	frlmelbas 21682	. . . . . . 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 692	. . . . . 6 ⊢ (𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ↔ (𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ 𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))))
125	124	anbi1i 624	. . . . 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 2926	. . . . . . 7 ⊢ (𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) ↔ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))
127	126	anbi2i 623	. . . . . 6 ⊢ (((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
128	127	anbi2i 623	. . . . 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 3072	. . 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 17168	. . . . . 6 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾s 𝐹)))
134	78, 133	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾s 𝐹)))
135	80	fveq2d 6830	. . . . 5 ⊢ (𝜑 → (Base‘(𝐸 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))
136	134, 135	eqtr2d 2765	. . . 4 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = 𝐹)
137	136	oveq1d 7368	. . 3 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) = (𝐹 ↑m (0...𝐷)))
138	93	crnggrpd 20151	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ Grp)
139	138	grpmndd 18844	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
140		subrgsubg 20481	. . . . . . . . . 10 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
141	9, 140	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
142		eqid 2729	. . . . . . . . . 10 ⊢ (0g‘𝐸) = (0g‘𝐸)
143	142	subg0cl 19032	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ 𝐹)
144	141, 143	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝐹)
145	5, 76, 142	ress0g 18655	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹)))
146	139, 144, 78, 145	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹)))
147	80	fveq2d 6830	. . . . . . 7 ⊢ (𝜑 → (0g‘(𝐸 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))
148	146, 147	eqtr2d 2765	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (0g‘𝐸))
149		extdgfialglem1.2	. . . . . 6 ⊢ 𝑍 = (0g‘𝐸)
150	148, 149	eqtr4di 2782	. . . . 5 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = 𝑍)
151	150	breq2d 5107	. . . 4 ⊢ (𝜑 → (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↔ 𝑎 finSupp 𝑍))
152		extdgfialglem1.3	. . . . . . . . . . 11 ⊢ · = (.r‘𝐸)
153	75, 79	sravsca 21104	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)))
154	152, 153	eqtr2id 2777	. . . . . . . . . 10 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = · )
155	154	ofeqd 7619	. . . . . . . . 9 ⊢ (𝜑 → ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = ∘f · )
156	155	oveqd 7370	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺) = (𝑎 ∘f · 𝐺))
157	156	oveq2d 7369	. . . . . . 7 ⊢ (𝜑 → (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f · 𝐺)))
158		ovexd 7388	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∘f · 𝐺) ∈ V)
159	10, 158, 2, 12, 79	gsumsra 33019	. . . . . . 7 ⊢ (𝜑 → (𝐸 Σg (𝑎 ∘f · 𝐺)) = (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f · 𝐺)))
160	157, 159	eqtr4d 2767	. . . . . 6 ⊢ (𝜑 → (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (𝐸 Σg (𝑎 ∘f · 𝐺)))
161	149	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑍 = (0g‘𝐸))
162	75, 161, 79	sralmod0 21111	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0g‘((subringAlg ‘𝐸)‘𝐹)))
163	162	eqcomd 2735	. . . . . 6 ⊢ (𝜑 → (0g‘((subringAlg ‘𝐸)‘𝐹)) = 𝑍)
164	160, 163	eqeq12d 2745	. . . . 5 ⊢ (𝜑 → ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ↔ (𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍))
165	150	sneqd 4591	. . . . . . 7 ⊢ (𝜑 → {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))} = {𝑍})
166	165	xpeq2d 5653	. . . . . 6 ⊢ (𝜑 → ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) = ((0...𝐷) × {𝑍}))
167	166	neeq2d 2985	. . . . 5 ⊢ (𝜑 → (𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) ↔ 𝑎 ≠ ((0...𝐷) × {𝑍})))
168	164, 167	anbi12d 632	. . . 4 ⊢ (𝜑 → (((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))
169	151, 168	anbi12d 632	. . 3 ⊢ (𝜑 → ((𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ (𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍})))))
170	137, 169	rexeqbidv 3311	. 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 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3438   ⊆ wss 3905  {csn 4579   class class class wbr 5095   ↦ cmpt 5176   × cxp 5621  dom cdm 5623  ran crn 5624  Fun wfun 6480  ⟶wf 6482  –1-1→wf1 6483  ‘cfv 6486  (class class class)co 7353   ∘_f cof 7615   ↑_m cmap 8760  Fincfn 8879   finSupp cfsupp 9270  ℝcr 11027  0cc0 11028  1c1 11029   + caddc 11031  ℝ^*cxr 11167   < clt 11168   ≤ cle 11169  ℕ₀cn0 12403  ...cfz 13429  ♯chash 14256  Basecbs 17139   ↾_s cress 17160  ._rcmulr 17181  Scalarcsca 17183   ·_𝑠 cvsca 17184  0_gc0g 17362   Σ_g cgsu 17363  Mndcmnd 18627  ._gcmg 18965  SubGrpcsubg 19018  mulGrpcmgp 20044  Ringcrg 20137  NzRingcnzr 20416  SubRingcsubrg 20473  DivRingcdr 20633  Fieldcfield 20634  SubDRingcsdrg 20690  LModclmod 20782  LBasisclbs 20997  LVecclvec 21025  subringAlg csra 21094   freeLMod cfrlm 21672   LIndF clindf 21730  LIndSclinds 21731  dimcldim 33584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-reg 9503  ax-inf2 9556  ax-ac2 10376  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-rpss 7663  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-tpos 8166  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-oadd 8399  df-er 8632  df-map 8762  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-sup 9351  df-oi 9421  df-r1 9679  df-rank 9680  df-dju 9816  df-card 9854  df-acn 9857  df-ac 10029  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-xnn0 12477  df-z 12491  df-dec 12611  df-uz 12755  df-fz 13430  df-fzo 13577  df-seq 13928  df-hash 14257  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17140  df-ress 17161  df-plusg 17193  df-mulr 17194  df-sca 17196  df-vsca 17197  df-ip 17198  df-tset 17199  df-ple 17200  df-ocomp 17201  df-ds 17202  df-hom 17204  df-cco 17205  df-0g 17364  df-gsum 17365  df-prds 17370  df-pws 17372  df-mre 17507  df-mrc 17508  df-mri 17509  df-acs 17510  df-proset 18219  df-drs 18220  df-poset 18238  df-ipo 18453  df-mgm 18533  df-sgrp 18612  df-mnd 18628  df-mhm 18676  df-submnd 18677  df-grp 18834  df-minusg 18835  df-sbg 18836  df-mulg 18966  df-subg 19021  df-ghm 19111  df-cntz 19215  df-cmn 19680  df-abl 19681  df-mgp 20045  df-rng 20057  df-ur 20086  df-ring 20139  df-cring 20140  df-oppr 20241  df-dvdsr 20261  df-unit 20262  df-invr 20292  df-nzr 20417  df-subrg 20474  df-drng 20635  df-field 20636  df-sdrg 20691  df-lmod 20784  df-lss 20854  df-lsp 20894  df-lmhm 20945  df-lbs 20998  df-lvec 21026  df-sra 21096  df-rgmod 21097  df-dsmm 21658  df-frlm 21673  df-uvc 21709  df-lindf 21732  df-linds 21733  df-dim 33585

This theorem is referenced by:  extdgfialg  33680