Theorem extdgfialglem1 34063

Description: Lemma for extdgfialg 34065. (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 780	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)))
2		extdgfialg.e	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐸 ∈ Field)
3	2	flddrngd 20828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ DivRing)
4		extdgfialg.f	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
5		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹)
6	5	sdrgdrng 20874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing)
7	4, 6	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
8		sdrgsubrg 20875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
9	4, 8	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
10		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
11	10, 5	sralvec 33956	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 ∈ DivRing ∧ (𝐸 ↾s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
12	3, 7, 9, 11	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
13	12	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
14	13	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → ((subringAlg ‘𝐸)‘𝐹) ∈ LVec)
15		extdgfialg.d	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))
16		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) = (LBasis‘((subringAlg ‘𝐸)‘𝐹))
17	16	dimval 33972	. . . . . . . . . . . . . . . 16 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐹)) = (♯‘𝑏))
18	15, 17	eqtrid 2810	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 = (♯‘𝑏))
19	14, 1, 18	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝐷 = (♯‘𝑏))
20		extdgfialg.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℕ0)
21	20	ad4antr 744	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝐷 ∈ ℕ0)
22	19, 21	eqeltrrd 2864	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝑏) ∈ ℕ0)
23		hashclb 14396	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ0))
24	23	biimpar 482	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ0) → 𝑏 ∈ Fin)
25	1, 22, 24	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → 𝑏 ∈ Fin)
26		hashss 14447	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ Fin ∧ ran 𝐺 ⊆ 𝑏) → (♯‘ran 𝐺) ≤ (♯‘𝑏))
27	25, 26	sylancom 599	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘ran 𝐺) ≤ (♯‘𝑏))
28		extdgfialglem1.r	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
29	28	dmeqi 5896	. . . . . . . . . . . . . 14 ⊢ dom 𝐺 = dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
30		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
31		ovexd 7447	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
32	30, 31	dmmptd 6682	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) = (0...𝐷))
33		ovexd 7447	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (0...𝐷) ∈ V)
34	32, 33	eqeltrd 2863	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) ∈ V)
35	29, 34	eqeltrid 2867	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom 𝐺 ∈ V)
36		hashf1rn 14390	. . . . . . . . . . . . 13 ⊢ ((dom 𝐺 ∈ V ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘ran 𝐺))
37	35, 36	sylancom 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘ran 𝐺))
38	37	ad3antrrr 742	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝐺) = (♯‘ran 𝐺))
39	27, 38, 19	3brtr4d 5144	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))) ∧ ran 𝐺 ⊆ 𝑏) → (♯‘𝐺) ≤ 𝐷)
40	16	islinds4 21966	. . . . . . . . . . . 12 ⊢ (((subringAlg ‘𝐸)‘𝐹) ∈ LVec → (ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)) ↔ ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏))
41	40	biimpa 481	. . . . . . . . . . 11 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LVec ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏)
42	13, 41	sylancom 599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ∃𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐹))ran 𝐺 ⊆ 𝑏)
43	39, 42	r19.29a 3173	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) ≤ 𝐷)
44	20	nn0red 12567	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℝ)
45	44	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 ∈ ℝ)
46	45	ltp1d 12146	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 < (𝐷 + 1))
47		fzfid 14011	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
48	47	mptexd 7224	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) ∈ V)
49	28, 48	eqeltrid 2867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ V)
50	49	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → 𝐺 ∈ V)
51		f1f 6776	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:dom 𝐺–1-1→V → 𝐺:dom 𝐺⟶V)
52	51	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → 𝐺:dom 𝐺⟶V)
53	52	ffund 6712	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → Fun 𝐺)
54		hashfundm 14481	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ V ∧ Fun 𝐺) → (♯‘𝐺) = (♯‘dom 𝐺))
55	50, 53, 54	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (♯‘dom 𝐺))
56	28, 31	dmmptd 6682	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → dom 𝐺 = (0...𝐷))
57	56	fveq2d 6887	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘dom 𝐺) = (♯‘(0...𝐷)))
58		hashfz0 14471	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ0 → (♯‘(0...𝐷)) = (𝐷 + 1))
59	20, 58	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘(0...𝐷)) = (𝐷 + 1))
60	59	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘(0...𝐷)) = (𝐷 + 1))
61	55, 57, 60	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → (♯‘𝐺) = (𝐷 + 1))
62	61	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) = (𝐷 + 1))
63	46, 62	breqtrrd 5140	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 < (♯‘𝐺))
64	45	rexrd 11260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐷 ∈ ℝ*)
65	50	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → 𝐺 ∈ V)
66		hashxrcl 14395	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ V → (♯‘𝐺) ∈ ℝ*)
67	65, 66	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (♯‘𝐺) ∈ ℝ*)
68	64, 67	xrltnled 11278	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → (𝐷 < (♯‘𝐺) ↔ ¬ (♯‘𝐺) ≤ 𝐷))
69	63, 68	mpbid 235	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) → ¬ (♯‘𝐺) ≤ 𝐷)
70	43, 69	pm2.65da 828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:dom 𝐺–1-1→V) → ¬ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))
71	70	ex 417	. . . . . . 7 ⊢ (𝜑 → (𝐺:dom 𝐺–1-1→V → ¬ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))))
72		imnan 404	. . . . . . 7 ⊢ ((𝐺:dom 𝐺–1-1→V → ¬ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))) ↔ ¬ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))))
73	71, 72	sylib 221	. . . . . 6 ⊢ (𝜑 → ¬ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹))))
74	12	lveclmodd 21209	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LMod)
75		eqidd 2764	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹))
76		extdgfialg.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐸)
77	76	sdrgss 20877	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
78	4, 77	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
79	78, 76	sseqtrdi 3978	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
80	75, 79	srasca 21282	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐸)‘𝐹)))
81		drngnzr 20835	. . . . . . . . 9 ⊢ ((𝐸 ↾s 𝐹) ∈ DivRing → (𝐸 ↾s 𝐹) ∈ NzRing)
82	7, 81	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ NzRing)
83	80, 82	eqeltrrd 2864	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ NzRing)
84		eqid 2763	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) = (Scalar‘((subringAlg ‘𝐸)‘𝐹))
85	84	islindf3 21957	. . . . . . 7 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ NzRing) → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))))
86	74, 83, 85	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ (𝐺:dom 𝐺–1-1→V ∧ ran 𝐺 ∈ (LIndS‘((subringAlg ‘𝐸)‘𝐹)))))
87	73, 86	mtbird 328	. . . . 5 ⊢ (𝜑 → ¬ 𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹))
88		ovexd 7447	. . . . . 6 ⊢ (𝜑 → (0...𝐷) ∈ V)
89		eqid 2763	. . . . . . . . 9 ⊢ (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) = (mulGrp‘((subringAlg ‘𝐸)‘𝐹))
90		eqid 2763	. . . . . . . . 9 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐹)) = (Base‘((subringAlg ‘𝐸)‘𝐹))
91	89, 90	mgpbas 20222	. . . . . . . 8 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐹)) = (Base‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))
92		eqid 2763	. . . . . . . 8 ⊢ (.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))) = (.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))
93	2	fldcrngd 20829	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ CRing)
94	93	crngringd 20329	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ Ring)
95	10, 76	sraring 21288	. . . . . . . . . . 11 ⊢ ((𝐸 ∈ Ring ∧ 𝐹 ⊆ 𝐵) → ((subringAlg ‘𝐸)‘𝐹) ∈ Ring)
96	94, 78, 95	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ Ring)
97	89	ringmgp 20322	. . . . . . . . . 10 ⊢ (((subringAlg ‘𝐸)‘𝐹) ∈ Ring → (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) ∈ Mnd)
98	96, 97	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) ∈ Mnd)
99	98	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (mulGrp‘((subringAlg ‘𝐸)‘𝐹)) ∈ Mnd)
100		fz0ssnn0 13652	. . . . . . . . . 10 ⊢ (0...𝐷) ⊆ ℕ0
101	100	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ0)
102	101	sselda 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ0)
103		extdgfialglem1.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
104	75, 79	srabase 21279	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐹)))
105	76, 104	eqtr2id 2811	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐸)‘𝐹)) = 𝐵)
106	103, 105	eleqtrrd 2866	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
107	106	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
108	91, 92, 99, 102, 107	mulgnn0cld 19162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ (Base‘((subringAlg ‘𝐸)‘𝐹)))
109	108, 28	fmptd 7111	. . . . . 6 ⊢ (𝜑 → 𝐺:(0...𝐷)⟶(Base‘((subringAlg ‘𝐸)‘𝐹)))
110		eqid 2763	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))
111		eqid 2763	. . . . . . 7 ⊢ (0g‘((subringAlg ‘𝐸)‘𝐹)) = (0g‘((subringAlg ‘𝐸)‘𝐹))
112		eqid 2763	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))
113		eqid 2763	. . . . . . 7 ⊢ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) = (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))
114	90, 84, 110, 111, 112, 113	islindf4 21969	. . . . . 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 1398	. . . . 5 ⊢ (𝜑 → (𝐺 LIndF ((subringAlg ‘𝐸)‘𝐹) ↔ ∀𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) → 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
116	87, 115	mtbid 327	. . . 4 ⊢ (𝜑 → ¬ ∀𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) → 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
117		rexanali 3119	. . . 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 237	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)))((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
119		fvex 6896	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐹)) ∈ V
120		ovex 7445	. . . . . . 7 ⊢ (0...𝐷) ∈ V
121		eqid 2763	. . . . . . . 8 ⊢ ((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷)) = ((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))
122		eqid 2763	. . . . . . . 8 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))
123	121, 122, 112, 113	frlmelbas 21887	. . . . . . 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 704	. . . . . 6 ⊢ (𝑎 ∈ (Base‘((Scalar‘((subringAlg ‘𝐸)‘𝐹)) freeLMod (0...𝐷))) ↔ (𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) ∧ 𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))))
125	124	anbi1i 635	. . . . 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 2959	. . . . . . 7 ⊢ (𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) ↔ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))
127	126	anbi2i 634	. . . . . 6 ⊢ (((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ ¬ 𝑎 = ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})))
128	127	anbi2i 634	. . . . 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 473	. . . . 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 304	. . . 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 3108	. . 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 221	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷))(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))))
133	5, 76	ressbas2 17299	. . . . . 6 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾s 𝐹)))
134	78, 133	syl 18	. . . . 5 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾s 𝐹)))
135	80	fveq2d 6887	. . . . 5 ⊢ (𝜑 → (Base‘(𝐸 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))
136	134, 135	eqtr2d 2799	. . . 4 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = 𝐹)
137	136	oveq1d 7427	. . 3 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↑m (0...𝐷)) = (𝐹 ↑m (0...𝐷)))
138	93	crnggrpd 20330	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ Grp)
139	138	grpmndd 19014	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
140		subrgsubg 20663	. . . . . . . . . 10 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
141	9, 140	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
142		eqid 2763	. . . . . . . . . 10 ⊢ (0g‘𝐸) = (0g‘𝐸)
143	142	subg0cl 19201	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ 𝐹)
144	141, 143	syl 18	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝐸) ∈ 𝐹)
145	5, 76, 142	ress0g 18821	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹)))
146	139, 144, 78, 145	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹)))
147	80	fveq2d 6887	. . . . . . 7 ⊢ (𝜑 → (0g‘(𝐸 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))))
148	146, 147	eqtr2d 2799	. . . . . 6 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = (0g‘𝐸))
149		extdgfialglem1.2	. . . . . 6 ⊢ 𝑍 = (0g‘𝐸)
150	148, 149	eqtr4di 2816	. . . . 5 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) = 𝑍)
151	150	breq2d 5122	. . . 4 ⊢ (𝜑 → (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ↔ 𝑎 finSupp 𝑍))
152		extdgfialglem1.3	. . . . . . . . . . 11 ⊢ · = (.r‘𝐸)
153	75, 79	sravsca 21283	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)))
154	152, 153	eqtr2id 2811	. . . . . . . . . 10 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = · )
155	154	ofeqd 7678	. . . . . . . . 9 ⊢ (𝜑 → ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹)) = ∘f · )
156	155	oveqd 7429	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺) = (𝑎 ∘f · 𝐺))
157	156	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f · 𝐺)))
158		ovexd 7447	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∘f · 𝐺) ∈ V)
159	10, 158, 2, 12, 79	gsumsra 33348	. . . . . . 7 ⊢ (𝜑 → (𝐸 Σg (𝑎 ∘f · 𝐺)) = (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f · 𝐺)))
160	157, 159	eqtr4d 2801	. . . . . 6 ⊢ (𝜑 → (((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (𝐸 Σg (𝑎 ∘f · 𝐺)))
161	149	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑍 = (0g‘𝐸))
162	75, 161, 79	sralmod0 21290	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0g‘((subringAlg ‘𝐸)‘𝐹)))
163	162	eqcomd 2769	. . . . . 6 ⊢ (𝜑 → (0g‘((subringAlg ‘𝐸)‘𝐹)) = 𝑍)
164	160, 163	eqeq12d 2779	. . . . 5 ⊢ (𝜑 → ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ↔ (𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍))
165	150	sneqd 4602	. . . . . . 7 ⊢ (𝜑 → {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))} = {𝑍})
166	165	xpeq2d 5693	. . . . . 6 ⊢ (𝜑 → ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) = ((0...𝐷) × {𝑍}))
167	166	neeq2d 3018	. . . . 5 ⊢ (𝜑 → (𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}) ↔ 𝑎 ≠ ((0...𝐷) × {𝑍})))
168	164, 167	anbi12d 643	. . . 4 ⊢ (𝜑 → (((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))})) ↔ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))
169	151, 168	anbi12d 643	. . 3 ⊢ (𝜑 → ((𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹))) ∧ ((((subringAlg ‘𝐸)‘𝐹) Σg (𝑎 ∘f ( ·𝑠 ‘((subringAlg ‘𝐸)‘𝐹))𝐺)) = (0g‘((subringAlg ‘𝐸)‘𝐹)) ∧ 𝑎 ≠ ((0...𝐷) × {(0g‘(Scalar‘((subringAlg ‘𝐸)‘𝐹)))}))) ↔ (𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍})))))
170	137, 169	rexeqbidv 3339	. 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 235	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3455   ⊆ wss 3906  {csn 4590   class class class wbr 5110   ↦ cmpt 5193   × cxp 5661  dom cdm 5663  ran crn 5664  Fun wfun 6532  ⟶wf 6534  –1-1→wf1 6535  ‘cfv 6538  (class class class)co 7412   ∘_f cof 7674   ↑_m cmap 8825  Fincfn 8944   finSupp cfsupp 9322  ℝcr 11100  0cc0 11101  1c1 11102   + caddc 11104  ℝ^*cxr 11243   < clt 11244   ≤ cle 11245  ℕ₀cn0 12505  ...cfz 13536  ♯chash 14368  Basecbs 17270   ↾_s cress 17291  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  0_gc0g 17493   Σ_g cgsu 17494  Mndcmnd 18793  ._gcmg 19134  SubGrpcsubg 19187  mulGrpcmgp 20217  Ringcrg 20316  NzRingcnzr 20596  SubRingcsubrg 20655  DivRingcdr 20814  Fieldcfield 20815  SubDRingcsdrg 20870  LModclmod 20962  LBasisclbs 21176  LVecclvec 21204  subringAlg csra 21273   freeLMod cfrlm 21877   LIndF clindf 21935  LIndSclinds 21936  dimcldim 33970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-reg 9555  ax-inf2 9611  ax-ac2 10448  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-iin 4960  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7676  df-rpss 7722  df-om 7864  df-1st 7987  df-2nd 7988  df-supp 8158  df-tpos 8223  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-2o 8455  df-oadd 8458  df-er 8695  df-map 8827  df-ixp 8897  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-fsupp 9323  df-sup 9403  df-oi 9473  df-r1 9737  df-rank 9738  df-dju 9888  df-card 9926  df-acn 9929  df-ac 10101  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-2 12304  df-3 12305  df-4 12306  df-5 12307  df-6 12308  df-7 12309  df-8 12310  df-9 12311  df-n0 12506  df-xnn0 12579  df-z 12593  df-dec 12713  df-uz 12864  df-fz 13537  df-fzo 13685  df-seq 14040  df-hash 14369  df-struct 17208  df-sets 17225  df-slot 17243  df-ndx 17255  df-base 17271  df-ress 17292  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ocomp 17332  df-ds 17333  df-hom 17335  df-cco 17336  df-0g 17495  df-gsum 17496  df-prds 17501  df-pws 17503  df-mre 17639  df-mrc 17640  df-mri 17641  df-acs 17642  df-proset 18351  df-drs 18352  df-poset 18370  df-ipo 18585  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-mhm 18842  df-submnd 18843  df-grp 19004  df-minusg 19005  df-sbg 19006  df-mulg 19135  df-subg 19190  df-ghm 19285  df-cntz 19388  df-cmn 19853  df-abl 19854  df-mgp 20218  df-rng 20232  df-ur 20265  df-ring 20318  df-cring 20319  df-oppr 20420  df-dvdsr 20440  df-unit 20441  df-invr 20471  df-nzr 20597  df-subrg 20656  df-drng 20816  df-field 20817  df-sdrg 20871  df-lmod 20964  df-lss 21034  df-lsp 21074  df-lmhm 21124  df-lbs 21177  df-lvec 21205  df-sra 21275  df-rgmod 21276  df-dsmm 21863  df-frlm 21878  df-uvc 21914  df-lindf 21937  df-linds 21938  df-dim 33971

This theorem is referenced by:  extdgfialg  34065