lfl1

Description: A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lfl1.d	$⊢ D = Scalar (W)$
	lfl1.o	$⊢ \underset{˙}{0} = 0_{D}$
	lfl1.u	$⊢ \underset{˙}{1} = 1_{D}$
	lfl1.v	$⊢ V = {Base}_{W}$
	lfl1.f	$⊢ F = LFnl (W)$
Assertion	lfl1	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to \exists x \in V G (x) = \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		lfl1.d	$⊢ D = Scalar (W)$
2		lfl1.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lfl1.u	$⊢ \underset{˙}{1} = 1_{D}$
4		lfl1.v	$⊢ V = {Base}_{W}$
5		lfl1.f	$⊢ F = LFnl (W)$
6		nne	$⊢ \neg G (z) \neq \underset{˙}{0} \leftrightarrow G (z) = \underset{˙}{0}$
7	6	ralbii	$⊢ \forall z \in V \neg G (z) \neq \underset{˙}{0} \leftrightarrow \forall z \in V G (z) = \underset{˙}{0}$
8		eqid	$⊢ {Base}_{D} = {Base}_{D}$
9	1 8 4 5	lflf	$⊢ (W \in LVec \land G \in F) \to G : V ⟶ {Base}_{D}$
10	9	ffnd	$⊢ (W \in LVec \land G \in F) \to G Fn V$
11		fconstfv	$⊢ G : V ⟶ \{\underset{˙}{0}\} \leftrightarrow (G Fn V \land \forall z \in V G (z) = \underset{˙}{0})$
12	11	simplbi2	$⊢ G Fn V \to (\forall z \in V G (z) = \underset{˙}{0} \to G : V ⟶ \{\underset{˙}{0}\})$
13	10 12	syl	$⊢ (W \in LVec \land G \in F) \to (\forall z \in V G (z) = \underset{˙}{0} \to G : V ⟶ \{\underset{˙}{0}\})$
14	2	fvexi	$⊢ \underset{˙}{0} \in V$
15	14	fconst2	$⊢ G : V ⟶ \{\underset{˙}{0}\} \leftrightarrow G = V \times \{\underset{˙}{0}\}$
16	13 15	syl6ib	$⊢ (W \in LVec \land G \in F) \to (\forall z \in V G (z) = \underset{˙}{0} \to G = V \times \{\underset{˙}{0}\})$
17	7 16	syl5bi	$⊢ (W \in LVec \land G \in F) \to (\forall z \in V \neg G (z) \neq \underset{˙}{0} \to G = V \times \{\underset{˙}{0}\})$
18	17	necon3ad	$⊢ (W \in LVec \land G \in F) \to (G \neq V \times \{\underset{˙}{0}\} \to \neg \forall z \in V \neg G (z) \neq \underset{˙}{0})$
19		dfrex2	$⊢ \exists z \in V G (z) \neq \underset{˙}{0} \leftrightarrow \neg \forall z \in V \neg G (z) \neq \underset{˙}{0}$
20	18 19	syl6ibr	$⊢ (W \in LVec \land G \in F) \to (G \neq V \times \{\underset{˙}{0}\} \to \exists z \in V G (z) \neq \underset{˙}{0})$
21	20	3impia	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to \exists z \in V G (z) \neq \underset{˙}{0}$
22		simp1l	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to W \in LVec$
23		lveclmod	$⊢ W \in LVec \to W \in LMod$
24	22 23	syl	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to W \in LMod$
25	1	lvecdrng	$⊢ W \in LVec \to D \in DivRing$
26	22 25	syl	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to D \in DivRing$
27		simp1r	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to G \in F$
28		simp2	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to z \in V$
29	1 8 4 5	lflcl	$⊢ (W \in LVec \land G \in F \land z \in V) \to G (z) \in {Base}_{D}$
30	22 27 28 29	syl3anc	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to G (z) \in {Base}_{D}$
31		simp3	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to G (z) \neq \underset{˙}{0}$
32		eqid	$⊢ {inv}_{r} (D) = {inv}_{r} (D)$
33	8 2 32	drnginvrcl	$⊢ (D \in DivRing \land G (z) \in {Base}_{D} \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (z)) \in {Base}_{D}$
34	26 30 31 33	syl3anc	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (z)) \in {Base}_{D}$
35		eqid	$⊢ \cdot_{W} = \cdot_{W}$
36	4 1 35 8	lmodvscl	$⊢ (W \in LMod \land {inv}_{r} (D) (G (z)) \in {Base}_{D} \land z \in V) \to {inv}_{r} (D) (G (z)) \cdot_{W} z \in V$
37	24 34 28 36	syl3anc	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (z)) \cdot_{W} z \in V$
38		eqid	$⊢ \cdot_{D} = \cdot_{D}$
39	1 8 38 4 35 5	lflmul	$⊢ (W \in LMod \land G \in F \land ({inv}_{r} (D) (G (z)) \in {Base}_{D} \land z \in V)) \to G ({inv}_{r} (D) (G (z)) \cdot_{W} z) = {inv}_{r} (D) (G (z)) \cdot_{D} G (z)$
40	24 27 34 28 39	syl112anc	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to G ({inv}_{r} (D) (G (z)) \cdot_{W} z) = {inv}_{r} (D) (G (z)) \cdot_{D} G (z)$
41	8 2 38 3 32	drnginvrl	$⊢ (D \in DivRing \land G (z) \in {Base}_{D} \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (z)) \cdot_{D} G (z) = \underset{˙}{1}$
42	26 30 31 41	syl3anc	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (z)) \cdot_{D} G (z) = \underset{˙}{1}$
43	40 42	eqtrd	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to G ({inv}_{r} (D) (G (z)) \cdot_{W} z) = \underset{˙}{1}$
44		fveqeq2	$⊢ x = {inv}_{r} (D) (G (z)) \cdot_{W} z \to (G (x) = \underset{˙}{1} \leftrightarrow G ({inv}_{r} (D) (G (z)) \cdot_{W} z) = \underset{˙}{1})$
45	44	rspcev	$⊢ ({inv}_{r} (D) (G (z)) \cdot_{W} z \in V \land G ({inv}_{r} (D) (G (z)) \cdot_{W} z) = \underset{˙}{1}) \to \exists x \in V G (x) = \underset{˙}{1}$
46	37 43 45	syl2anc	$⊢ ((W \in LVec \land G \in F) \land z \in V \land G (z) \neq \underset{˙}{0}) \to \exists x \in V G (x) = \underset{˙}{1}$
47	46	rexlimdv3a	$⊢ (W \in LVec \land G \in F) \to (\exists z \in V G (z) \neq \underset{˙}{0} \to \exists x \in V G (x) = \underset{˙}{1})$
48	47	3adant3	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to (\exists z \in V G (z) \neq \underset{˙}{0} \to \exists x \in V G (x) = \underset{˙}{1})$
49	21 48	mpd	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to \exists x \in V G (x) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem lfl1

Proof