extdgfialglem1

	Ref	Expression
Hypotheses	extdgfialg.b	$⊢ B = {Base}_{E}$
	extdgfialg.d	$⊢ D = \dim (subringAlg (E) (F))$
	extdgfialg.e	$⊢ φ \to E \in Field$
	extdgfialg.f	$⊢ φ \to F \in SubDRing (E)$
	extdgfialg.1	$⊢ φ \to D \in ℕ_{0}$
	extdgfialglem1.2	$⊢ Z = 0_{E}$
	extdgfialglem1.3	$⊢ \underset{˙}{\cdot} = \cdot_{E}$
	extdgfialglem1.r	$⊢ G = (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X)$
	extdgfialglem1.4	$⊢ φ \to X \in B$
Assertion	extdgfialglem1	$⊢ φ \to \exists a \in (F^{(0 \dots D)}) ({finSupp}_{Z} (a) \land (\sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = Z \land a \neq (0 \dots D) \times \{Z\}))$

Proof

Step	Hyp	Ref	Expression
1		extdgfialg.b	$⊢ B = {Base}_{E}$
2		extdgfialg.d	$⊢ D = \dim (subringAlg (E) (F))$
3		extdgfialg.e	$⊢ φ \to E \in Field$
4		extdgfialg.f	$⊢ φ \to F \in SubDRing (E)$
5		extdgfialg.1	$⊢ φ \to D \in ℕ_{0}$
6		extdgfialglem1.2	$⊢ Z = 0_{E}$
7		extdgfialglem1.3	$⊢ \underset{˙}{\cdot} = \cdot_{E}$
8		extdgfialglem1.r	$⊢ G = (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X)$
9		extdgfialglem1.4	$⊢ φ \to X \in B$
10		simplr	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to b \in LBasis (subringAlg (E) (F))$
11	3	flddrngd	$⊢ φ \to E \in DivRing$
12		eqid	$⊢ E ↾_{𝑠} F = E ↾_{𝑠} F$
13	12	sdrgdrng	$⊢ F \in SubDRing (E) \to E ↾_{𝑠} F \in DivRing$
14	4 13	syl	$⊢ φ \to E ↾_{𝑠} F \in DivRing$
15		sdrgsubrg	$⊢ F \in SubDRing (E) \to F \in SubRing (E)$
16	4 15	syl	$⊢ φ \to F \in SubRing (E)$
17		eqid	$⊢ subringAlg (E) (F) = subringAlg (E) (F)$
18	17 12	sralvec	$⊢ (E \in DivRing \land E ↾_{𝑠} F \in DivRing \land F \in SubRing (E)) \to subringAlg (E) (F) \in LVec$
19	11 14 16 18	syl3anc	$⊢ φ \to subringAlg (E) (F) \in LVec$
20	19	ad2antrr	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to subringAlg (E) (F) \in LVec$
21	20	ad2antrr	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to subringAlg (E) (F) \in LVec$
22		eqid	$⊢ LBasis (subringAlg (E) (F)) = LBasis (subringAlg (E) (F))$
23	22	dimval	$⊢ (subringAlg (E) (F) \in LVec \land b \in LBasis (subringAlg (E) (F))) \to \dim (subringAlg (E) (F)) = \|b\|$
24	2 23	eqtrid	$⊢ (subringAlg (E) (F) \in LVec \land b \in LBasis (subringAlg (E) (F))) \to D = \|b\|$
25	21 10 24	syl2anc	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to D = \|b\|$
26	5	ad4antr	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to D \in ℕ_{0}$
27	25 26	eqeltrrd	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to \|b\| \in ℕ_{0}$
28		hashclb	$⊢ b \in LBasis (subringAlg (E) (F)) \to (b \in Fin \leftrightarrow \|b\| \in ℕ_{0})$
29	28	biimpar	$⊢ (b \in LBasis (subringAlg (E) (F)) \land \|b\| \in ℕ_{0}) \to b \in Fin$
30	10 27 29	syl2anc	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to b \in Fin$
31		hashss	$⊢ (b \in Fin \land ran G \subseteq b) \to \|ran G\| \leq \|b\|$
32	30 31	sylancom	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to \|ran G\| \leq \|b\|$
33	8	dmeqi	$⊢ dom G = dom (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X)$
34		eqid	$⊢ (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X) = (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X)$
35		ovexd	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land n \in (0 \dots D)) \to n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X \in V$
36	34 35	dmmptd	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to dom (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X) = (0 \dots D)$
37		ovexd	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to (0 \dots D) \in V$
38	36 37	eqeltrd	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to dom (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X) \in V$
39	33 38	eqeltrid	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to dom G \in V$
40		hashf1rn	$⊢ (dom G \in V \land G : dom G \underset{1-1}{⟶} V) \to \|G\| = \|ran G\|$
41	39 40	sylancom	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to \|G\| = \|ran G\|$
42	41	ad3antrrr	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to \|G\| = \|ran G\|$
43	32 42 25	3brtr4d	$⊢ ((((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \land b \in LBasis (subringAlg (E) (F))) \land ran G \subseteq b) \to \|G\| \leq D$
44	22	islinds4	$⊢ subringAlg (E) (F) \in LVec \to (ran G \in LIndS (subringAlg (E) (F)) \leftrightarrow \exists b \in LBasis (subringAlg (E) (F)) ran G \subseteq b)$
45	44	biimpa	$⊢ (subringAlg (E) (F) \in LVec \land ran G \in LIndS (subringAlg (E) (F))) \to \exists b \in LBasis (subringAlg (E) (F)) ran G \subseteq b$
46	20 45	sylancom	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to \exists b \in LBasis (subringAlg (E) (F)) ran G \subseteq b$
47	43 46	r19.29a	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to \|G\| \leq D$
48	5	nn0red	$⊢ φ \to D \in ℝ$
49	48	ad2antrr	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to D \in ℝ$
50	49	ltp1d	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to D < D + 1$
51		fzfid	$⊢ φ \to (0 \dots D) \in Fin$
52	51	mptexd	$⊢ φ \to (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X) \in V$
53	8 52	eqeltrid	$⊢ φ \to G \in V$
54	53	adantr	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to G \in V$
55		f1f	$⊢ G : dom G \underset{1-1}{⟶} V \to G : dom G ⟶ V$
56	55	adantl	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to G : dom G ⟶ V$
57	56	ffund	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to Fun G$
58		hashfundm	$⊢ (G \in V \land Fun G) \to \|G\| = \|dom G\|$
59	54 57 58	syl2anc	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to \|G\| = \|dom G\|$
60	8 35	dmmptd	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to dom G = (0 \dots D)$
61	60	fveq2d	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to \|dom G\| = \|(0 \dots D)\|$
62		hashfz0	$⊢ D \in ℕ_{0} \to \|(0 \dots D)\| = D + 1$
63	5 62	syl	$⊢ φ \to \|(0 \dots D)\| = D + 1$
64	63	adantr	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to \|(0 \dots D)\| = D + 1$
65	59 61 64	3eqtrd	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to \|G\| = D + 1$
66	65	adantr	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to \|G\| = D + 1$
67	50 66	breqtrrd	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to D < \|G\|$
68	49	rexrd	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to D \in ℝ^{*}$
69	54	adantr	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to G \in V$
70		hashxrcl	$⊢ G \in V \to \|G\| \in ℝ^{*}$
71	69 70	syl	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to \|G\| \in ℝ^{*}$
72	68 71	xrltnled	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to (D < \|G\| \leftrightarrow \neg \|G\| \leq D)$
73	67 72	mpbid	$⊢ ((φ \land G : dom G \underset{1-1}{⟶} V) \land ran G \in LIndS (subringAlg (E) (F))) \to \neg \|G\| \leq D$
74	47 73	pm2.65da	$⊢ (φ \land G : dom G \underset{1-1}{⟶} V) \to \neg ran G \in LIndS (subringAlg (E) (F))$
75	74	ex	$⊢ φ \to (G : dom G \underset{1-1}{⟶} V \to \neg ran G \in LIndS (subringAlg (E) (F)))$
76		imnan	$⊢ (G : dom G \underset{1-1}{⟶} V \to \neg ran G \in LIndS (subringAlg (E) (F))) \leftrightarrow \neg (G : dom G \underset{1-1}{⟶} V \land ran G \in LIndS (subringAlg (E) (F)))$
77	75 76	sylib	$⊢ φ \to \neg (G : dom G \underset{1-1}{⟶} V \land ran G \in LIndS (subringAlg (E) (F)))$
78	19	lveclmodd	$⊢ φ \to subringAlg (E) (F) \in LMod$
79		eqidd	$⊢ φ \to subringAlg (E) (F) = subringAlg (E) (F)$
80	1	sdrgss	$⊢ F \in SubDRing (E) \to F \subseteq B$
81	4 80	syl	$⊢ φ \to F \subseteq B$
82	81 1	sseqtrdi	$⊢ φ \to F \subseteq {Base}_{E}$
83	79 82	srasca	$⊢ φ \to E ↾_{𝑠} F = Scalar (subringAlg (E) (F))$
84		drngnzr	$⊢ E ↾_{𝑠} F \in DivRing \to E ↾_{𝑠} F \in NzRing$
85	14 84	syl	$⊢ φ \to E ↾_{𝑠} F \in NzRing$
86	83 85	eqeltrrd	$⊢ φ \to Scalar (subringAlg (E) (F)) \in NzRing$
87		eqid	$⊢ Scalar (subringAlg (E) (F)) = Scalar (subringAlg (E) (F))$
88	87	islindf3	$⊢ (subringAlg (E) (F) \in LMod \land Scalar (subringAlg (E) (F)) \in NzRing) \to (G LIndF subringAlg (E) (F) \leftrightarrow (G : dom G \underset{1-1}{⟶} V \land ran G \in LIndS (subringAlg (E) (F))))$
89	78 86 88	syl2anc	$⊢ φ \to (G LIndF subringAlg (E) (F) \leftrightarrow (G : dom G \underset{1-1}{⟶} V \land ran G \in LIndS (subringAlg (E) (F))))$
90	77 89	mtbird	$⊢ φ \to \neg G LIndF subringAlg (E) (F)$
91		ovexd	$⊢ φ \to (0 \dots D) \in V$
92		eqid	$⊢ {mulGrp}_{subringAlg (E) (F)} = {mulGrp}_{subringAlg (E) (F)}$
93		eqid	$⊢ {Base}_{subringAlg (E) (F)} = {Base}_{subringAlg (E) (F)}$
94	92 93	mgpbas	$⊢ {Base}_{subringAlg (E) (F)} = {Base}_{{mulGrp}_{subringAlg (E) (F)}}$
95		eqid	$⊢ \cdot_{{mulGrp}_{subringAlg (E) (F)}} = \cdot_{{mulGrp}_{subringAlg (E) (F)}}$
96	3	fldcrngd	$⊢ φ \to E \in CRing$
97	96	crngringd	$⊢ φ \to E \in Ring$
98	17 1	sraring	$⊢ (E \in Ring \land F \subseteq B) \to subringAlg (E) (F) \in Ring$
99	97 81 98	syl2anc	$⊢ φ \to subringAlg (E) (F) \in Ring$
100	92	ringmgp	$⊢ subringAlg (E) (F) \in Ring \to {mulGrp}_{subringAlg (E) (F)} \in Mnd$
101	99 100	syl	$⊢ φ \to {mulGrp}_{subringAlg (E) (F)} \in Mnd$
102	101	adantr	$⊢ (φ \land n \in (0 \dots D)) \to {mulGrp}_{subringAlg (E) (F)} \in Mnd$
103		fz0ssnn0	$⊢ (0 \dots D) \subseteq ℕ_{0}$
104	103	a1i	$⊢ φ \to (0 \dots D) \subseteq ℕ_{0}$
105	104	sselda	$⊢ (φ \land n \in (0 \dots D)) \to n \in ℕ_{0}$
106	79 82	srabase	$⊢ φ \to {Base}_{E} = {Base}_{subringAlg (E) (F)}$
107	1 106	eqtr2id	$⊢ φ \to {Base}_{subringAlg (E) (F)} = B$
108	9 107	eleqtrrd	$⊢ φ \to X \in {Base}_{subringAlg (E) (F)}$
109	108	adantr	$⊢ (φ \land n \in (0 \dots D)) \to X \in {Base}_{subringAlg (E) (F)}$
110	94 95 102 105 109	mulgnn0cld	$⊢ (φ \land n \in (0 \dots D)) \to n \cdot_{{mulGrp}_{subringAlg (E) (F)}} X \in {Base}_{subringAlg (E) (F)}$
111	110 8	fmptd	$⊢ φ \to G : (0 \dots D) ⟶ {Base}_{subringAlg (E) (F)}$
112		eqid	$⊢ \cdot_{subringAlg (E) (F)} = \cdot_{subringAlg (E) (F)}$
113		eqid	$⊢ 0_{subringAlg (E) (F)} = 0_{subringAlg (E) (F)}$
114		eqid	$⊢ 0_{Scalar (subringAlg (E) (F))} = 0_{Scalar (subringAlg (E) (F))}$
115		eqid	$⊢ {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} = {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))}$
116	93 87 112 113 114 115	islindf4	$⊢ (subringAlg (E) (F) \in LMod \land (0 \dots D) \in V \land G : (0 \dots D) ⟶ {Base}_{subringAlg (E) (F)}) \to (G LIndF subringAlg (E) (F) \leftrightarrow \forall a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \to a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}))$
117	78 91 111 116	syl3anc	$⊢ φ \to (G LIndF subringAlg (E) (F) \leftrightarrow \forall a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \to a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}))$
118	90 117	mtbid	$⊢ φ \to \neg \forall a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \to a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})$
119		rexanali	$⊢ \exists a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}) \leftrightarrow \neg \forall a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \to a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})$
120	118 119	sylibr	$⊢ φ \to \exists a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})$
121		fvex	$⊢ Scalar (subringAlg (E) (F)) \in V$
122		ovex	$⊢ (0 \dots D) \in V$
123		eqid	$⊢ Scalar (subringAlg (E) (F)) freeLMod (0 \dots D) = Scalar (subringAlg (E) (F)) freeLMod (0 \dots D)$
124		eqid	$⊢ {Base}_{Scalar (subringAlg (E) (F))} = {Base}_{Scalar (subringAlg (E) (F))}$
125	123 124 114 115	frlmelbas	$⊢ (Scalar (subringAlg (E) (F)) \in V \land (0 \dots D) \in V) \to (a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} \leftrightarrow (a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) \land {finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a)))$
126	121 122 125	mp2an	$⊢ a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} \leftrightarrow (a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) \land {finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a))$
127	126	anbi1i	$⊢ (a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})) \leftrightarrow ((a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) \land {finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a)) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}))$
128		df-ne	$⊢ a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\} \leftrightarrow \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}$
129	128	anbi2i	$⊢ (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}) \leftrightarrow (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})$
130	129	anbi2i	$⊢ (a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})) \leftrightarrow (a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}))$
131		anass	$⊢ ((a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) \land {finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a)) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})) \leftrightarrow (a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) \land ({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})))$
132	127 130 131	3bitr3i	$⊢ (a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})) \leftrightarrow (a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) \land ({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})))$
133	132	rexbii2	$⊢ \exists a \in {Base}_{(Scalar (subringAlg (E) (F)) freeLMod (0 \dots D))} (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land \neg a = (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}) \leftrightarrow \exists a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) ({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}))$
134	120 133	sylib	$⊢ φ \to \exists a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) ({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}))$
135	12 1	ressbas2	$⊢ F \subseteq B \to F = {Base}_{(E ↾_{𝑠} F)}$
136	81 135	syl	$⊢ φ \to F = {Base}_{(E ↾_{𝑠} F)}$
137	83	fveq2d	$⊢ φ \to {Base}_{(E ↾_{𝑠} F)} = {Base}_{Scalar (subringAlg (E) (F))}$
138	136 137	eqtr2d	$⊢ φ \to {Base}_{Scalar (subringAlg (E) (F))} = F$
139	138	oveq1d	$⊢ φ \to {Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)} = F^{(0 \dots D)}$
140	96	crnggrpd	$⊢ φ \to E \in Grp$
141	140	grpmndd	$⊢ φ \to E \in Mnd$
142		subrgsubg	$⊢ F \in SubRing (E) \to F \in SubGrp (E)$
143	16 142	syl	$⊢ φ \to F \in SubGrp (E)$
144		eqid	$⊢ 0_{E} = 0_{E}$
145	144	subg0cl	$⊢ F \in SubGrp (E) \to 0_{E} \in F$
146	143 145	syl	$⊢ φ \to 0_{E} \in F$
147	12 1 144	ress0g	$⊢ (E \in Mnd \land 0_{E} \in F \land F \subseteq B) \to 0_{E} = 0_{(E ↾_{𝑠} F)}$
148	141 146 81 147	syl3anc	$⊢ φ \to 0_{E} = 0_{(E ↾_{𝑠} F)}$
149	83	fveq2d	$⊢ φ \to 0_{(E ↾_{𝑠} F)} = 0_{Scalar (subringAlg (E) (F))}$
150	148 149	eqtr2d	$⊢ φ \to 0_{Scalar (subringAlg (E) (F))} = 0_{E}$
151	150 6	eqtr4di	$⊢ φ \to 0_{Scalar (subringAlg (E) (F))} = Z$
152	151	breq2d	$⊢ φ \to ({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \leftrightarrow {finSupp}_{Z} (a))$
153	79 82	sravsca	$⊢ φ \to \cdot_{E} = \cdot_{subringAlg (E) (F)}$
154	7 153	eqtr2id	$⊢ φ \to \cdot_{subringAlg (E) (F)} = \underset{˙}{\cdot}$
155	154	ofeqd	$⊢ φ \to \circ_{f} \cdot_{subringAlg (E) (F)} = \circ_{f} \underset{˙}{\cdot}$
156	155	oveqd	$⊢ φ \to a {\cdot_{subringAlg (E) (F)}}_{f} G = a {\underset{˙}{\cdot}}_{f} G$
157	156	oveq2d	$⊢ φ \to \sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = \sum_{subringAlg (E) (F)} (a {\underset{˙}{\cdot}}_{f} G)$
158		ovexd	$⊢ φ \to a {\underset{˙}{\cdot}}_{f} G \in V$
159	17 158 3 19 82	gsumsra	$⊢ φ \to \sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = \sum_{subringAlg (E) (F)} (a {\underset{˙}{\cdot}}_{f} G)$
160	157 159	eqtr4d	$⊢ φ \to \sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = \sum_{E} (a {\underset{˙}{\cdot}}_{f} G)$
161	6	a1i	$⊢ φ \to Z = 0_{E}$
162	79 161 82	sralmod0	$⊢ φ \to Z = 0_{subringAlg (E) (F)}$
163	162	eqcomd	$⊢ φ \to 0_{subringAlg (E) (F)} = Z$
164	160 163	eqeq12d	$⊢ φ \to (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \leftrightarrow \sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = Z)$
165	151	sneqd	$⊢ φ \to \{0_{Scalar (subringAlg (E) (F))}\} = \{Z\}$
166	165	xpeq2d	$⊢ φ \to (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\} = (0 \dots D) \times \{Z\}$
167	166	neeq2d	$⊢ φ \to (a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\} \leftrightarrow a \neq (0 \dots D) \times \{Z\})$
168	164 167	anbi12d	$⊢ φ \to ((\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\}) \leftrightarrow (\sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = Z \land a \neq (0 \dots D) \times \{Z\}))$
169	152 168	anbi12d	$⊢ φ \to (({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})) \leftrightarrow ({finSupp}_{Z} (a) \land (\sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = Z \land a \neq (0 \dots D) \times \{Z\})))$
170	139 169	rexeqbidv	$⊢ φ \to (\exists a \in ({Base}_{Scalar (subringAlg (E) (F))}^{(0 \dots D)}) ({finSupp}_{0_{Scalar (subringAlg (E) (F))}} (a) \land (\sum_{subringAlg (E) (F)} (a {\cdot_{subringAlg (E) (F)}}_{f} G) = 0_{subringAlg (E) (F)} \land a \neq (0 \dots D) \times \{0_{Scalar (subringAlg (E) (F))}\})) \leftrightarrow \exists a \in (F^{(0 \dots D)}) ({finSupp}_{Z} (a) \land (\sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = Z \land a \neq (0 \dots D) \times \{Z\})))$
171	134 170	mpbid	$⊢ φ \to \exists a \in (F^{(0 \dots D)}) ({finSupp}_{Z} (a) \land (\sum_{E} (a {\underset{˙}{\cdot}}_{f} G) = Z \land a \neq (0 \dots D) \times \{Z\}))$

Metamath Proof Explorer

Theorem extdgfialglem1

Proof