Theorem fta1blem

Description: Lemma for fta1b . (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	fta1b.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	fta1b.b	$$⊢B={\mathrm{Base}}_P$$
	fta1b.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	fta1b.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	fta1b.w	$$⊢W=0_R$$
	fta1b.z	$$⊢\underset{\dot{}}{0}=0_P$$
	fta1blem.k	$$⊢K={\mathrm{Base}}_R$$
	fta1blem.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	fta1blem.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	fta1blem.s	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	fta1blem.1	$$⊢\phi \to R\in \mathrm{CRing}$$
	fta1blem.2	$$⊢\phi \to M\in K$$
	fta1blem.3	$$⊢\phi \to N\in K$$
	fta1blem.4	$$⊢\phi \to M\underset{\dot{}}{\times }N=W$$
	fta1blem.5	$$⊢\phi \to M\ne W$$
	fta1blem.6	$$⊢\phi \to \left(M\underset{\dot{}}{·}X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le D\left(M\underset{\dot{}}{·}X\right)\right)$$
Assertion	fta1blem	$$⊢\phi \to N=W$$

Proof

Step	Hyp	Ref	Expression
1		fta1b.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		fta1b.b	$$⊢B={\mathrm{Base}}_P$$
3		fta1b.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
4		fta1b.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
5		fta1b.w	$$⊢W=0_R$$
6		fta1b.z	$$⊢\underset{\dot{}}{0}=0_P$$
7		fta1blem.k	$$⊢K={\mathrm{Base}}_R$$
8		fta1blem.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
9		fta1blem.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
10		fta1blem.s	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
11		fta1blem.1	$$⊢\phi \to R\in \mathrm{CRing}$$
12		fta1blem.2	$$⊢\phi \to M\in K$$
13		fta1blem.3	$$⊢\phi \to N\in K$$
14		fta1blem.4	$$⊢\phi \to M\underset{\dot{}}{\times }N=W$$
15		fta1blem.5	$$⊢\phi \to M\ne W$$
16		fta1blem.6	$$⊢\phi \to \left(M\underset{\dot{}}{·}X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le D\left(M\underset{\dot{}}{·}X\right)\right)$$
17	4 9 7 1 2 11 13	evl1vard	$$⊢\phi \to \left(X\in B\wedge O\left(X\right)\left(N\right)=N\right)$$
18	4 1 7 2 11 13 17 12 10 8	evl1vsd	$$⊢\phi \to \left(M\underset{\dot{}}{·}X\in B\wedge O\left(M\underset{\dot{}}{·}X\right)\left(N\right)=M\underset{\dot{}}{\times }N\right)$$
19	18	simprd	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)\left(N\right)=M\underset{\dot{}}{\times }N$$
20	19 14	eqtrd	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)\left(N\right)=W$$
21		eqid	$$⊢R{\uparrow }_{𝑠}K=R{\uparrow }_{𝑠}K$$
22		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
23	7	fvexi	$$⊢K\in \mathrm{V}$$
24	23	a1i	$$⊢\phi \to K\in \mathrm{V}$$
25	4 1 21 7	evl1rhm	$$⊢R\in \mathrm{CRing}\to O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)$$
26	11 25	syl	$$⊢\phi \to O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)$$
27	2 22	rhmf	$$⊢O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)\to O:B⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
28	26 27	syl	$$⊢\phi \to O:B⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
29	18	simpld	$$⊢\phi \to M\underset{\dot{}}{·}X\in B$$
30	28 29	ffvelcdmd	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
31	21 7 22 11 24 30	pwselbas	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right):K⟶K$$
32	31	ffnd	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)FnK$$
33		fniniseg	$$⊢O\left(M\underset{\dot{}}{·}X\right)FnK\to \left(N\in {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\leftrightarrow \left(N\in K\wedge O\left(M\underset{\dot{}}{·}X\right)\left(N\right)=W\right)\right)$$
34	32 33	syl	$$⊢\phi \to \left(N\in {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\leftrightarrow \left(N\in K\wedge O\left(M\underset{\dot{}}{·}X\right)\left(N\right)=W\right)\right)$$
35	13 20 34	mpbir2and	$$⊢\phi \to N\in {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
36		fvex	$$⊢O\left(M\underset{\dot{}}{·}X\right)\in \mathrm{V}$$
37	36	cnvex	$$⊢{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\in \mathrm{V}$$
38	37	imaex	$$⊢{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{V}$$
39	38	a1i	$$⊢\phi \to {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{V}$$
40		1nn0	$$⊢1\in {\mathbb{N}}_0$$
41	40	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
42		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
43	11 42	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
44	9 1 2	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
45	43 44	syl	$$⊢\phi \to X\in B$$
46		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
47	46 2	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
48		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
49	47 48	mulg1	$$⊢X\in B\to 1{\cdot }_{{\mathrm{mulGrp}}_P}X=X$$
50	45 49	syl	$$⊢\phi \to 1{\cdot }_{{\mathrm{mulGrp}}_P}X=X$$
51	50	oveq2d	$$⊢\phi \to M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=M\underset{\dot{}}{·}X$$
52	5 7 1 9 10 46 48	coe1tmfv1	$$⊢\left(R\in \mathrm{Ring}\wedge M\in K\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)\left(1\right)=M$$
53	43 12 41 52	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)\left(1\right)=M$$
54	1 6 5	coe1z	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)={\mathbb{N}}_0\times \left\{W\right\}$$
55	43 54	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)={\mathbb{N}}_0\times \left\{W\right\}$$
56	55	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)\left(1\right)=\left({\mathbb{N}}_0\times \left\{W\right\}\right)\left(1\right)$$
57	5	fvexi	$$⊢W\in \mathrm{V}$$
58	57	fvconst2	$$⊢1\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{W\right\}\right)\left(1\right)=W$$
59	40 58	ax-mp	$$⊢\left({\mathbb{N}}_0\times \left\{W\right\}\right)\left(1\right)=W$$
60	56 59	eqtrdi	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)\left(1\right)=W$$
61	15 53 60	3netr4d	$$⊢\phi \to {\mathrm{coe}}_1\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)\left(1\right)\ne {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)\left(1\right)$$
62		fveq2	$$⊢M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=\underset{\dot{}}{0}\to {\mathrm{coe}}_1\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)={\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)$$
63	62	fveq1d	$$⊢M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=\underset{\dot{}}{0}\to {\mathrm{coe}}_1\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)\left(1\right)={\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)\left(1\right)$$
64	63	necon3i	$$⊢{\mathrm{coe}}_1\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)\left(1\right)\ne {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)\left(1\right)\to M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\ne \underset{\dot{}}{0}$$
65	61 64	syl	$$⊢\phi \to M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\ne \underset{\dot{}}{0}$$
66	51 65	eqnetrrd	$$⊢\phi \to M\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}$$
67		eldifsn	$$⊢M\underset{\dot{}}{·}X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(M\underset{\dot{}}{·}X\in B\wedge M\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}\right)$$
68	29 66 67	sylanbrc	$$⊢\phi \to M\underset{\dot{}}{·}X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
69	68 16	mpd	$$⊢\phi \to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le D\left(M\underset{\dot{}}{·}X\right)$$
70	51	fveq2d	$$⊢\phi \to D\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)=D\left(M\underset{\dot{}}{·}X\right)$$
71	3 7 1 9 10 46 48 5	deg1tm	$$⊢\left(R\in \mathrm{Ring}\wedge \left(M\in K\wedge M\ne W\right)\wedge 1\in {\mathbb{N}}_0\right)\to D\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)=1$$
72	43 12 15 41 71	syl121anc	$$⊢\phi \to D\left(M\underset{\dot{}}{·}\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)\right)=1$$
73	70 72	eqtr3d	$$⊢\phi \to D\left(M\underset{\dot{}}{·}X\right)=1$$
74	69 73	breqtrd	$$⊢\phi \to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le 1$$
75		hashbnd	$$⊢\left({O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{V}\wedge 1\in {\mathbb{N}}_0\wedge \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le 1\right)\to {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{Fin}$$
76	39 41 74 75	syl3anc	$$⊢\phi \to {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{Fin}$$
77	7 5	ring0cl	$$⊢R\in \mathrm{Ring}\to W\in K$$
78	43 77	syl	$$⊢\phi \to W\in K$$
79		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
80	1 79 7 2	ply1sclf	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right):K⟶B$$
81	43 80	syl	$$⊢\phi \to \mathrm{algSc}\left(P\right):K⟶B$$
82	81 12	ffvelcdmd	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(M\right)\in B$$
83		eqid	$$⊢{\cdot }_P={\cdot }_P$$
84		eqid	$$⊢{\cdot }_{\left(R{\uparrow }_{𝑠}K\right)}={\cdot }_{\left(R{\uparrow }_{𝑠}K\right)}$$
85	2 83 84	rhmmul	$$⊢\left(O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)\wedge \mathrm{algSc}\left(P\right)\left(M\right)\in B\wedge X\in B\right)\to O\left(\mathrm{algSc}\left(P\right)\left(M\right){\cdot }_{P}X\right)=O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right){\cdot }_{\left(R{\uparrow }_{𝑠}K\right)}O\left(X\right)$$
86	26 82 45 85	syl3anc	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right){\cdot }_{P}X\right)=O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right){\cdot }_{\left(R{\uparrow }_{𝑠}K\right)}O\left(X\right)$$
87	1	ply1assa	$$⊢R\in \mathrm{CRing}\to P\in \mathrm{AssAlg}$$
88	11 87	syl	$$⊢\phi \to P\in \mathrm{AssAlg}$$
89	1	ply1sca	$$⊢R\in \mathrm{CRing}\to R=\mathrm{Scalar}\left(P\right)$$
90	11 89	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
91	90	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
92	7 91	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
93	12 92	eleqtrd	$$⊢\phi \to M\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
94		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
95		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
96	79 94 95 2 83 10	asclmul1	$$⊢\left(P\in \mathrm{AssAlg}\wedge M\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge X\in B\right)\to \mathrm{algSc}\left(P\right)\left(M\right){\cdot }_{P}X=M\underset{\dot{}}{·}X$$
97	88 93 45 96	syl3anc	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(M\right){\cdot }_{P}X=M\underset{\dot{}}{·}X$$
98	97	fveq2d	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right){\cdot }_{P}X\right)=O\left(M\underset{\dot{}}{·}X\right)$$
99	28 82	ffvelcdmd	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
100	28 45	ffvelcdmd	$$⊢\phi \to O\left(X\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
101	21 22 11 24 99 100 8 84	pwsmulrval	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right){\cdot }_{\left(R{\uparrow }_{𝑠}K\right)}O\left(X\right)=O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right){\underset{\dot{}}{\times }}_{f}O\left(X\right)$$
102	4 1 7 79	evl1sca	$$⊢\left(R\in \mathrm{CRing}\wedge M\in K\right)\to O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right)=K\times \left\{M\right\}$$
103	11 12 102	syl2anc	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right)=K\times \left\{M\right\}$$
104	4 9 7	evl1var	$$⊢R\in \mathrm{CRing}\to O\left(X\right)={\mathrm{I}\upharpoonright }_K$$
105	11 104	syl	$$⊢\phi \to O\left(X\right)={\mathrm{I}\upharpoonright }_K$$
106	103 105	oveq12d	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right){\underset{\dot{}}{\times }}_{f}O\left(X\right)=\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)$$
107	101 106	eqtrd	$$⊢\phi \to O\left(\mathrm{algSc}\left(P\right)\left(M\right)\right){\cdot }_{\left(R{\uparrow }_{𝑠}K\right)}O\left(X\right)=\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)$$
108	86 98 107	3eqtr3d	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)=\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)$$
109	108	fveq1d	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)\left(W\right)=\left(\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)\right)\left(W\right)$$
110		fnconstg	$$⊢M\in K\to \left(K\times \left\{M\right\}\right)FnK$$
111	12 110	syl	$$⊢\phi \to \left(K\times \left\{M\right\}\right)FnK$$
112		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_K\right)FnK$$
113	112	a1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_K\right)FnK$$
114		fnfvof	$$⊢\left(\left(\left(K\times \left\{M\right\}\right)FnK\wedge \left({\mathrm{I}\upharpoonright }_K\right)FnK\right)\wedge \left(K\in \mathrm{V}\wedge W\in K\right)\right)\to \left(\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)\right)\left(W\right)=\left(K\times \left\{M\right\}\right)\left(W\right)\underset{\dot{}}{\times }\left({\mathrm{I}\upharpoonright }_K\right)\left(W\right)$$
115	111 113 24 78 114	syl22anc	$$⊢\phi \to \left(\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)\right)\left(W\right)=\left(K\times \left\{M\right\}\right)\left(W\right)\underset{\dot{}}{\times }\left({\mathrm{I}\upharpoonright }_K\right)\left(W\right)$$
116		fvconst2g	$$⊢\left(M\in K\wedge W\in K\right)\to \left(K\times \left\{M\right\}\right)\left(W\right)=M$$
117	12 78 116	syl2anc	$$⊢\phi \to \left(K\times \left\{M\right\}\right)\left(W\right)=M$$
118		fvresi	$$⊢W\in K\to \left({\mathrm{I}\upharpoonright }_K\right)\left(W\right)=W$$
119	78 118	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_K\right)\left(W\right)=W$$
120	117 119	oveq12d	$$⊢\phi \to \left(K\times \left\{M\right\}\right)\left(W\right)\underset{\dot{}}{\times }\left({\mathrm{I}\upharpoonright }_K\right)\left(W\right)=M\underset{\dot{}}{\times }W$$
121	7 8 5	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge M\in K\right)\to M\underset{\dot{}}{\times }W=W$$
122	43 12 121	syl2anc	$$⊢\phi \to M\underset{\dot{}}{\times }W=W$$
123	120 122	eqtrd	$$⊢\phi \to \left(K\times \left\{M\right\}\right)\left(W\right)\underset{\dot{}}{\times }\left({\mathrm{I}\upharpoonright }_K\right)\left(W\right)=W$$
124	115 123	eqtrd	$$⊢\phi \to \left(\left(K\times \left\{M\right\}\right){\underset{\dot{}}{\times }}_f\left({\mathrm{I}\upharpoonright }_K\right)\right)\left(W\right)=W$$
125	109 124	eqtrd	$$⊢\phi \to O\left(M\underset{\dot{}}{·}X\right)\left(W\right)=W$$
126		fniniseg	$$⊢O\left(M\underset{\dot{}}{·}X\right)FnK\to \left(W\in {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\leftrightarrow \left(W\in K\wedge O\left(M\underset{\dot{}}{·}X\right)\left(W\right)=W\right)\right)$$
127	32 126	syl	$$⊢\phi \to \left(W\in {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\leftrightarrow \left(W\in K\wedge O\left(M\underset{\dot{}}{·}X\right)\left(W\right)=W\right)\right)$$
128	78 125 127	mpbir2and	$$⊢\phi \to W\in {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
129	128	snssd	$$⊢\phi \to \left\{W\right\}\subseteq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
130		hashsng	$$⊢W\in K\to \left|\left\{W\right\}\right|=1$$
131	78 130	syl	$$⊢\phi \to \left|\left\{W\right\}\right|=1$$
132		ssdomg	$$⊢{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{V}\to \left(\left\{W\right\}\subseteq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\to \left\{W\right\}\preccurlyeq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right)$$
133	38 129 132	mpsyl	$$⊢\phi \to \left\{W\right\}\preccurlyeq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
134		snfi	$$⊢\left\{W\right\}\in \mathrm{Fin}$$
135		hashdom	$$⊢\left(\left\{W\right\}\in \mathrm{Fin}\wedge {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{V}\right)\to \left(\left|\left\{W\right\}\right|\le \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\leftrightarrow \left\{W\right\}\preccurlyeq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right)$$
136	134 38 135	mp2an	$$⊢\left|\left\{W\right\}\right|\le \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\leftrightarrow \left\{W\right\}\preccurlyeq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
137	133 136	sylibr	$$⊢\phi \to \left|\left\{W\right\}\right|\le \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|$$
138	131 137	eqbrtrrd	$$⊢\phi \to 1\le \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|$$
139		hashcl	$$⊢{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{Fin}\to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\in {\mathbb{N}}_0$$
140	76 139	syl	$$⊢\phi \to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\in {\mathbb{N}}_0$$
141	140	nn0red	$$⊢\phi \to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\in ℝ$$
142		1re	$$⊢1\in ℝ$$
143		letri3	$$⊢\left(\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\in ℝ\wedge 1\in ℝ\right)\to \left(\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|=1\leftrightarrow \left(\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le 1\wedge 1\le \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\right)\right)$$
144	141 142 143	sylancl	$$⊢\phi \to \left(\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|=1\leftrightarrow \left(\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\le 1\wedge 1\le \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\right)\right)$$
145	74 138 144	mpbir2and	$$⊢\phi \to \left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|=1$$
146	131 145	eqtr4d	$$⊢\phi \to \left|\left\{W\right\}\right|=\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|$$
147		hashen	$$⊢\left(\left\{W\right\}\in \mathrm{Fin}\wedge {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{Fin}\right)\to \left(\left|\left\{W\right\}\right|=\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\leftrightarrow \left\{W\right\}\approx {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right)$$
148	134 76 147	sylancr	$$⊢\phi \to \left(\left|\left\{W\right\}\right|=\left|{O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right|\leftrightarrow \left\{W\right\}\approx {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right)$$
149	146 148	mpbid	$$⊢\phi \to \left\{W\right\}\approx {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
150		fisseneq	$$⊢\left({O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\in \mathrm{Fin}\wedge \left\{W\right\}\subseteq {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\wedge \left\{W\right\}\approx {O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]\right)\to \left\{W\right\}={O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
151	76 129 149 150	syl3anc	$$⊢\phi \to \left\{W\right\}={O\left(M\underset{\dot{}}{·}X\right)}^{-1}\left[\left\{W\right\}\right]$$
152	35 151	eleqtrrd	$$⊢\phi \to N\in \left\{W\right\}$$
153		elsni	$$⊢N\in \left\{W\right\}\to N=W$$
154	152 153	syl	$$⊢\phi \to N=W$$