Theorem prdsinvlem

Description: Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsinvlem.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsinvlem.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsinvlem.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	prdsinvlem.s	$$⊢\phi \to S\in V$$
	prdsinvlem.i	$$⊢\phi \to I\in W$$
	prdsinvlem.r	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
	prdsinvlem.f	$$⊢\phi \to F\in B$$
	prdsinvlem.z	$$⊢\underset{\dot{}}{0}=0_{𝑔}\circ R$$
	prdsinvlem.n	$$⊢N=\left(y\in I⟼{inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\right)$$
Assertion	prdsinvlem	$$⊢\phi \to \left(N\in B\wedge N\underset{\dot{}}{+}F=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsinvlem.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsinvlem.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsinvlem.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
4		prdsinvlem.s	$$⊢\phi \to S\in V$$
5		prdsinvlem.i	$$⊢\phi \to I\in W$$
6		prdsinvlem.r	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
7		prdsinvlem.f	$$⊢\phi \to F\in B$$
8		prdsinvlem.z	$$⊢\underset{\dot{}}{0}=0_{𝑔}\circ R$$
9		prdsinvlem.n	$$⊢N=\left(y\in I⟼{inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\right)$$
10	6	ffvelrnda	$$⊢\left(\phi \wedge y\in I\right)\to R\left(y\right)\in \mathrm{Grp}$$
11	4	adantr	$$⊢\left(\phi \wedge y\in I\right)\to S\in V$$
12	5	adantr	$$⊢\left(\phi \wedge y\in I\right)\to I\in W$$
13	6	ffnd	$$⊢\phi \to RFnI$$
14	13	adantr	$$⊢\left(\phi \wedge y\in I\right)\to RFnI$$
15	7	adantr	$$⊢\left(\phi \wedge y\in I\right)\to F\in B$$
16		simpr	$$⊢\left(\phi \wedge y\in I\right)\to y\in I$$
17	1 2 11 12 14 15 16	prdsbasprj	$$⊢\left(\phi \wedge y\in I\right)\to F\left(y\right)\in {\mathrm{Base}}_{R\left(y\right)}$$
18		eqid	$$⊢{\mathrm{Base}}_{R\left(y\right)}={\mathrm{Base}}_{R\left(y\right)}$$
19		eqid	$$⊢{inv}_g\left(R\left(y\right)\right)={inv}_g\left(R\left(y\right)\right)$$
20	18 19	grpinvcl	$$⊢\left(R\left(y\right)\in \mathrm{Grp}\wedge F\left(y\right)\in {\mathrm{Base}}_{R\left(y\right)}\right)\to {inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\in {\mathrm{Base}}_{R\left(y\right)}$$
21	10 17 20	syl2anc	$$⊢\left(\phi \wedge y\in I\right)\to {inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\in {\mathrm{Base}}_{R\left(y\right)}$$
22	21	ralrimiva	$$⊢\phi \to \forall y\in I{inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\in {\mathrm{Base}}_{R\left(y\right)}$$
23	1 2 4 5 13	prdsbasmpt	$$⊢\phi \to \left(\left(y\in I⟼{inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\right)\in B\leftrightarrow \forall y\in I{inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\in {\mathrm{Base}}_{R\left(y\right)}\right)$$
24	22 23	mpbird	$$⊢\phi \to \left(y\in I⟼{inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)\right)\in B$$
25	9 24	eqeltrid	$$⊢\phi \to N\in B$$
26	6	ffvelrnda	$$⊢\left(\phi \wedge x\in I\right)\to R\left(x\right)\in \mathrm{Grp}$$
27	4	adantr	$$⊢\left(\phi \wedge x\in I\right)\to S\in V$$
28	5	adantr	$$⊢\left(\phi \wedge x\in I\right)\to I\in W$$
29	13	adantr	$$⊢\left(\phi \wedge x\in I\right)\to RFnI$$
30	7	adantr	$$⊢\left(\phi \wedge x\in I\right)\to F\in B$$
31		simpr	$$⊢\left(\phi \wedge x\in I\right)\to x\in I$$
32	1 2 27 28 29 30 31	prdsbasprj	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
33		eqid	$$⊢{\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{R\left(x\right)}$$
34		eqid	$$⊢{+}_{R\left(x\right)}={+}_{R\left(x\right)}$$
35		eqid	$$⊢0_{R\left(x\right)}=0_{R\left(x\right)}$$
36		eqid	$$⊢{inv}_g\left(R\left(x\right)\right)={inv}_g\left(R\left(x\right)\right)$$
37	33 34 35 36	grplinv	$$⊢\left(R\left(x\right)\in \mathrm{Grp}\wedge F\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\right)\to {inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right){+}_{R\left(x\right)}F\left(x\right)=0_{R\left(x\right)}$$
38	26 32 37	syl2anc	$$⊢\left(\phi \wedge x\in I\right)\to {inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right){+}_{R\left(x\right)}F\left(x\right)=0_{R\left(x\right)}$$
39		2fveq3	$$⊢y=x\to {inv}_g\left(R\left(y\right)\right)={inv}_g\left(R\left(x\right)\right)$$
40		fveq2	$$⊢y=x\to F\left(y\right)=F\left(x\right)$$
41	39 40	fveq12d	$$⊢y=x\to {inv}_g\left(R\left(y\right)\right)\left(F\left(y\right)\right)={inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right)$$
42		fvex	$$⊢{inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right)\in \mathrm{V}$$
43	41 9 42	fvmpt	$$⊢x\in I\to N\left(x\right)={inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right)$$
44	43	adantl	$$⊢\left(\phi \wedge x\in I\right)\to N\left(x\right)={inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right)$$
45	44	oveq1d	$$⊢\left(\phi \wedge x\in I\right)\to N\left(x\right){+}_{R\left(x\right)}F\left(x\right)={inv}_g\left(R\left(x\right)\right)\left(F\left(x\right)\right){+}_{R\left(x\right)}F\left(x\right)$$
46	8	fveq1i	$$⊢\underset{\dot{}}{0}\left(x\right)=\left(0_{𝑔}\circ R\right)\left(x\right)$$
47		fvco2	$$⊢\left(RFnI\wedge x\in I\right)\to \left(0_{𝑔}\circ R\right)\left(x\right)=0_{R\left(x\right)}$$
48	13 47	sylan	$$⊢\left(\phi \wedge x\in I\right)\to \left(0_{𝑔}\circ R\right)\left(x\right)=0_{R\left(x\right)}$$
49	46 48	syl5eq	$$⊢\left(\phi \wedge x\in I\right)\to \underset{\dot{}}{0}\left(x\right)=0_{R\left(x\right)}$$
50	38 45 49	3eqtr4d	$$⊢\left(\phi \wedge x\in I\right)\to N\left(x\right){+}_{R\left(x\right)}F\left(x\right)=\underset{\dot{}}{0}\left(x\right)$$
51	50	mpteq2dva	$$⊢\phi \to \left(x\in I⟼N\left(x\right){+}_{R\left(x\right)}F\left(x\right)\right)=\left(x\in I⟼\underset{\dot{}}{0}\left(x\right)\right)$$
52	1 2 4 5 13 25 7 3	prdsplusgval	$$⊢\phi \to N\underset{\dot{}}{+}F=\left(x\in I⟼N\left(x\right){+}_{R\left(x\right)}F\left(x\right)\right)$$
53		fn0g	$$⊢0_{𝑔}Fn\mathrm{V}$$
54		ssv	$$⊢\mathrm{ran}R\subseteq \mathrm{V}$$
55	54	a1i	$$⊢\phi \to \mathrm{ran}R\subseteq \mathrm{V}$$
56		fnco	$$⊢\left(0_{𝑔}Fn\mathrm{V}\wedge RFnI\wedge \mathrm{ran}R\subseteq \mathrm{V}\right)\to \left(0_{𝑔}\circ R\right)FnI$$
57	53 13 55 56	mp3an2i	$$⊢\phi \to \left(0_{𝑔}\circ R\right)FnI$$
58	8	fneq1i	$$⊢\underset{\dot{}}{0}FnI\leftrightarrow \left(0_{𝑔}\circ R\right)FnI$$
59	57 58	sylibr	$$⊢\phi \to \underset{\dot{}}{0}FnI$$
60		dffn5	$$⊢\underset{\dot{}}{0}FnI\leftrightarrow \underset{\dot{}}{0}=\left(x\in I⟼\underset{\dot{}}{0}\left(x\right)\right)$$
61	59 60	sylib	$$⊢\phi \to \underset{\dot{}}{0}=\left(x\in I⟼\underset{\dot{}}{0}\left(x\right)\right)$$
62	51 52 61	3eqtr4d	$$⊢\phi \to N\underset{\dot{}}{+}F=\underset{\dot{}}{0}$$
63	25 62	jca	$$⊢\phi \to \left(N\in B\wedge N\underset{\dot{}}{+}F=\underset{\dot{}}{0}\right)$$