Theorem islshpkrN

Description: The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be U = ( Kg ) or ( Kg ) = U as in lshpkrex ? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lshpset2.v	$$⊢V={\mathrm{Base}}_W$$
	lshpset2.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lshpset2.z	$$⊢\underset{\dot{}}{0}=0_D$$
	lshpset2.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshpset2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lshpset2.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
Assertion	islshpkrN	$$⊢W\in \mathrm{LVec}\to \left(U\in H\leftrightarrow \exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lshpset2.v	$$⊢V={\mathrm{Base}}_W$$
2		lshpset2.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
3		lshpset2.z	$$⊢\underset{\dot{}}{0}=0_D$$
4		lshpset2.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
5		lshpset2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
6		lshpset2.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
7	1 2 3 4 5 6	lshpset2N	$$⊢W\in \mathrm{LVec}\to H=\left\{s|\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\right\}$$
8	7	eleq2d	$$⊢W\in \mathrm{LVec}\to \left(U\in H\leftrightarrow U\in \left\{s|\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\right\}\right)$$
9		elex	$$⊢U\in \left\{s|\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\right\}\to U\in \mathrm{V}$$
10	9	adantl	$$⊢\left(W\in \mathrm{LVec}\wedge U\in \left\{s|\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\right\}\right)\to U\in \mathrm{V}$$
11		fvex	$$⊢K\left(g\right)\in \mathrm{V}$$
12		eleq1	$$⊢U=K\left(g\right)\to \left(U\in \mathrm{V}\leftrightarrow K\left(g\right)\in \mathrm{V}\right)$$
13	11 12	mpbiri	$$⊢U=K\left(g\right)\to U\in \mathrm{V}$$
14	13	adantl	$$⊢\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\to U\in \mathrm{V}$$
15	14	rexlimivw	$$⊢\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\to U\in \mathrm{V}$$
16	15	adantl	$$⊢\left(W\in \mathrm{LVec}\wedge \exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)\to U\in \mathrm{V}$$
17		eqeq1	$$⊢s=U\to \left(s=K\left(g\right)\leftrightarrow U=K\left(g\right)\right)$$
18	17	anbi2d	$$⊢s=U\to \left(\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\leftrightarrow \left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)$$
19	18	rexbidv	$$⊢s=U\to \left(\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\leftrightarrow \exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)$$
20	19	elabg	$$⊢U\in \mathrm{V}\to \left(U\in \left\{s|\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\right\}\leftrightarrow \exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)$$
21	10 16 20	pm5.21nd	$$⊢W\in \mathrm{LVec}\to \left(U\in \left\{s|\exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge s=K\left(g\right)\right)\right\}\leftrightarrow \exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)$$
22	8 21	bitrd	$$⊢W\in \mathrm{LVec}\to \left(U\in H\leftrightarrow \exists g\in F\left(g\ne V\times \left\{\underset{\dot{}}{0}\right\}\wedge U=K\left(g\right)\right)\right)$$