Theorem lcfl7N

Description: Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 4-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcfl6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcfl6.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcfl6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcfl6.v	$$⊢V={\mathrm{Base}}_U$$
	lcfl6.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcfl6.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lcfl6.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcfl6.r	$$⊢R={\mathrm{Base}}_S$$
	lcfl6.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcfl6.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcfl6.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcfl6.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcfl6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcfl6.g	$$⊢\phi \to G\in F$$
Assertion	lcfl7N	$$⊢\phi \to \left(G\in C\leftrightarrow \left(L\left(G\right)=V\vee \exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcfl6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfl6.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfl6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfl6.v	$$⊢V={\mathrm{Base}}_U$$
5		lcfl6.a	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcfl6.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		lcfl6.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
8		lcfl6.r	$$⊢R={\mathrm{Base}}_S$$
9		lcfl6.z	$$⊢\underset{\dot{}}{0}=0_U$$
10		lcfl6.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
11		lcfl6.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
12		lcfl6.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
13		lcfl6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		lcfl6.g	$$⊢\phi \to G\in F$$
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	lcfl6	$$⊢\phi \to \left(G\in C\leftrightarrow \left(L\left(G\right)=V\vee \exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)\right)$$
16	13	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		eqid	$$⊢\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)$$
18		eqid	$$⊢\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)$$
19		simplrl	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
20		simplrr	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
21		simprl	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)$$
22		eqeq1	$$⊢v=u\to \left(v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)$$
23	22	rexbidv	$$⊢v=u\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)$$
24	23	riotabidv	$$⊢v=u\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)$$
25		oveq1	$$⊢k=l\to k\underset{\dot{}}{·}x=l\underset{\dot{}}{·}x$$
26	25	oveq2d	$$⊢k=l\to w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)$$
27	26	eqeq2d	$$⊢k=l\to \left(u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
28	27	rexbidv	$$⊢k=l\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
29		oveq1	$$⊢w=z\to w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)$$
30	29	eqeq2d	$$⊢w=z\to \left(u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\leftrightarrow u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
31	30	cbvrexvw	$$⊢\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)$$
32	28 31	bitrdi	$$⊢k=l\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
33	32	cbvriotavw	$$⊢\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
34	24 33	eqtrdi	$$⊢v=u\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
35	34	cbvmptv	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)$$
36	21 35	eqtrdi	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to G=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)$$
37		simprr	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)$$
38		eqeq1	$$⊢v=u\to \left(v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)$$
39	38	rexbidv	$$⊢v=u\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)$$
40	39	riotabidv	$$⊢v=u\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)$$
41		oveq1	$$⊢k=l\to k\underset{\dot{}}{·}y=l\underset{\dot{}}{·}y$$
42	41	oveq2d	$$⊢k=l\to w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)$$
43	42	eqeq2d	$$⊢k=l\to \left(u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
44	43	rexbidv	$$⊢k=l\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
45		oveq1	$$⊢w=z\to w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)$$
46	45	eqeq2d	$$⊢w=z\to \left(u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\leftrightarrow u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
47	46	cbvrexvw	$$⊢\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)$$
48	44 47	bitrdi	$$⊢k=l\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
49	48	cbvriotavw	$$⊢\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
50	40 49	eqtrdi	$$⊢v=u\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
51	50	cbvmptv	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)$$
52	37 51	eqtrdi	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to G=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)$$
53	36 52	eqtr3d	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to \left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)$$
54	1 2 3 4 5 6 7 8 9 10 11 16 17 18 19 20 53	lcfl7lem	$$⊢\left(\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)\to x=y$$
55	54	ex	$$⊢\left(\phi \wedge \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\to \left(\left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\to x=y\right)$$
56	55	ralrimivva	$$⊢\phi \to \forall x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(\left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\to x=y\right)$$
57	56	a1d	$$⊢\phi \to \left(\exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\to \forall x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(\left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\to x=y\right)\right)$$
58	57	ancld	$$⊢\phi \to \left(\exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\to \left(\exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge \forall x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(\left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\to x=y\right)\right)\right)$$
59		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
60	59	fveq2d	$$⊢x=y\to \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)=\underset{\dot{}}{\perp }\left(\left\{y\right\}\right)$$
61		oveq2	$$⊢x=y\to k\underset{\dot{}}{·}x=k\underset{\dot{}}{·}y$$
62	61	oveq2d	$$⊢x=y\to w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)$$
63	62	eqeq2d	$$⊢x=y\to \left(v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)$$
64	60 63	rexeqbidv	$$⊢x=y\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)$$
65	64	riotabidv	$$⊢x=y\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)$$
66	65	mpteq2dv	$$⊢x=y\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)$$
67	66	eqeq2d	$$⊢x=y\to \left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\leftrightarrow G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)$$
68	67	reu4	$$⊢\exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\leftrightarrow \left(\exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge \forall x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(\left(G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\wedge G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\to x=y\right)\right)$$
69	58 68	imbitrrdi	$$⊢\phi \to \left(\exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\to \exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
70		reurex	$$⊢\exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\to \exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)$$
71	69 70	impbid1	$$⊢\phi \to \left(\exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\leftrightarrow \exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
72	71	orbi2d	$$⊢\phi \to \left(\left(L\left(G\right)=V\vee \exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)\leftrightarrow \left(L\left(G\right)=V\vee \exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)\right)$$
73	15 72	bitrd	$$⊢\phi \to \left(G\in C\leftrightarrow \left(L\left(G\right)=V\vee \exists !x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)\right)$$