Theorem fidomndrnglem

Description: Lemma for fidomndrng . (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	fidomndrng.b	$$⊢B={\mathrm{Base}}_R$$
	fidomndrng.z	$$⊢\underset{\dot{}}{0}=0_R$$
	fidomndrng.o	$$⊢\underset{\dot{}}{1}=1_R$$
	fidomndrng.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	fidomndrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	fidomndrng.r	$$⊢\phi \to R\in \mathrm{Domn}$$
	fidomndrng.x	$$⊢\phi \to B\in \mathrm{Fin}$$
	fidomndrng.a	$$⊢\phi \to A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	fidomndrng.f	$$⊢F=\left(x\in B⟼x\underset{\dot{}}{·}A\right)$$
Assertion	fidomndrnglem	$$⊢\phi \to A\underset{\dot{}}{\parallel }\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		fidomndrng.b	$$⊢B={\mathrm{Base}}_R$$
2		fidomndrng.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		fidomndrng.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		fidomndrng.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
5		fidomndrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		fidomndrng.r	$$⊢\phi \to R\in \mathrm{Domn}$$
7		fidomndrng.x	$$⊢\phi \to B\in \mathrm{Fin}$$
8		fidomndrng.a	$$⊢\phi \to A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9		fidomndrng.f	$$⊢F=\left(x\in B⟼x\underset{\dot{}}{·}A\right)$$
10	8	eldifad	$$⊢\phi \to A\in B$$
11		eldifsni	$$⊢A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to A\ne \underset{\dot{}}{0}$$
12	8 11	syl	$$⊢\phi \to A\ne \underset{\dot{}}{0}$$
13	12	ad2antrr	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge F\left(y\right)=\underset{\dot{}}{0}\right)\to A\ne \underset{\dot{}}{0}$$
14		oveq1	$$⊢x=y\to x\underset{\dot{}}{·}A=y\underset{\dot{}}{·}A$$
15		ovex	$$⊢y\underset{\dot{}}{·}A\in \mathrm{V}$$
16	14 9 15	fvmpt	$$⊢y\in B\to F\left(y\right)=y\underset{\dot{}}{·}A$$
17	16	adantl	$$⊢\left(\phi \wedge y\in B\right)\to F\left(y\right)=y\underset{\dot{}}{·}A$$
18	17	eqeq1d	$$⊢\left(\phi \wedge y\in B\right)\to \left(F\left(y\right)=\underset{\dot{}}{0}\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
19	6	adantr	$$⊢\left(\phi \wedge y\in B\right)\to R\in \mathrm{Domn}$$
20		simpr	$$⊢\left(\phi \wedge y\in B\right)\to y\in B$$
21	10	adantr	$$⊢\left(\phi \wedge y\in B\right)\to A\in B$$
22	1 5 2	domneq0	$$⊢\left(R\in \mathrm{Domn}\wedge y\in B\wedge A\in B\right)\to \left(y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\leftrightarrow \left(y=\underset{\dot{}}{0}\vee A=\underset{\dot{}}{0}\right)\right)$$
23	19 20 21 22	syl3anc	$$⊢\left(\phi \wedge y\in B\right)\to \left(y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\leftrightarrow \left(y=\underset{\dot{}}{0}\vee A=\underset{\dot{}}{0}\right)\right)$$
24	18 23	bitrd	$$⊢\left(\phi \wedge y\in B\right)\to \left(F\left(y\right)=\underset{\dot{}}{0}\leftrightarrow \left(y=\underset{\dot{}}{0}\vee A=\underset{\dot{}}{0}\right)\right)$$
25	24	biimpa	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge F\left(y\right)=\underset{\dot{}}{0}\right)\to \left(y=\underset{\dot{}}{0}\vee A=\underset{\dot{}}{0}\right)$$
26	25	ord	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge F\left(y\right)=\underset{\dot{}}{0}\right)\to \left(\neg y=\underset{\dot{}}{0}\to A=\underset{\dot{}}{0}\right)$$
27	26	necon1ad	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge F\left(y\right)=\underset{\dot{}}{0}\right)\to \left(A\ne \underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)$$
28	13 27	mpd	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge F\left(y\right)=\underset{\dot{}}{0}\right)\to y=\underset{\dot{}}{0}$$
29	28	ex	$$⊢\left(\phi \wedge y\in B\right)\to \left(F\left(y\right)=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)$$
30	29	ralrimiva	$$⊢\phi \to \forall y\in B\left(F\left(y\right)=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)$$
31		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
32	6 31	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
33	1 5	ringrghm	$$⊢\left(R\in \mathrm{Ring}\wedge A\in B\right)\to \left(x\in B⟼x\underset{\dot{}}{·}A\right)\in \left(R\mathrm{GrpHom}R\right)$$
34	32 10 33	syl2anc	$$⊢\phi \to \left(x\in B⟼x\underset{\dot{}}{·}A\right)\in \left(R\mathrm{GrpHom}R\right)$$
35	9 34	eqeltrid	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}R\right)$$
36	1 1 2 2	ghmf1	$$⊢F\in \left(R\mathrm{GrpHom}R\right)\to \left(F:B\underset{1-1}{⟶}B\leftrightarrow \forall y\in B\left(F\left(y\right)=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
37	35 36	syl	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}B\leftrightarrow \forall y\in B\left(F\left(y\right)=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
38	30 37	mpbird	$$⊢\phi \to F:B\underset{1-1}{⟶}B$$
39		enrefg	$$⊢B\in \mathrm{Fin}\to B\approx B$$
40	7 39	syl	$$⊢\phi \to B\approx B$$
41		f1finf1o	$$⊢\left(B\approx B\wedge B\in \mathrm{Fin}\right)\to \left(F:B\underset{1-1}{⟶}B\leftrightarrow F:B\underset{1-1\; onto}{⟶}B\right)$$
42	40 7 41	syl2anc	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}B\leftrightarrow F:B\underset{1-1\; onto}{⟶}B\right)$$
43	38 42	mpbid	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}B$$
44		f1ocnv	$$⊢F:B\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}B$$
45		f1of	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}B\to F^{-1}:B⟶B$$
46	43 44 45	3syl	$$⊢\phi \to F^{-1}:B⟶B$$
47	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
48	32 47	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
49	46 48	ffvelcdmd	$$⊢\phi \to F^{-1}\left(\underset{\dot{}}{1}\right)\in B$$
50	1 4 5	dvdsrmul	$$⊢\left(A\in B\wedge F^{-1}\left(\underset{\dot{}}{1}\right)\in B\right)\to A\underset{\dot{}}{\parallel }\left(F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A\right)$$
51	10 49 50	syl2anc	$$⊢\phi \to A\underset{\dot{}}{\parallel }\left(F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A\right)$$
52		oveq1	$$⊢y=F^{-1}\left(\underset{\dot{}}{1}\right)\to y\underset{\dot{}}{·}A=F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A$$
53	14	cbvmptv	$$⊢\left(x\in B⟼x\underset{\dot{}}{·}A\right)=\left(y\in B⟼y\underset{\dot{}}{·}A\right)$$
54	9 53	eqtri	$$⊢F=\left(y\in B⟼y\underset{\dot{}}{·}A\right)$$
55		ovex	$$⊢F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A\in \mathrm{V}$$
56	52 54 55	fvmpt	$$⊢F^{-1}\left(\underset{\dot{}}{1}\right)\in B\to F\left(F^{-1}\left(\underset{\dot{}}{1}\right)\right)=F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A$$
57	49 56	syl	$$⊢\phi \to F\left(F^{-1}\left(\underset{\dot{}}{1}\right)\right)=F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A$$
58		f1ocnvfv2	$$⊢\left(F:B\underset{1-1\; onto}{⟶}B\wedge \underset{\dot{}}{1}\in B\right)\to F\left(F^{-1}\left(\underset{\dot{}}{1}\right)\right)=\underset{\dot{}}{1}$$
59	43 48 58	syl2anc	$$⊢\phi \to F\left(F^{-1}\left(\underset{\dot{}}{1}\right)\right)=\underset{\dot{}}{1}$$
60	57 59	eqtr3d	$$⊢\phi \to F^{-1}\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A=\underset{\dot{}}{1}$$
61	51 60	breqtrd	$$⊢\phi \to A\underset{\dot{}}{\parallel }\underset{\dot{}}{1}$$