Theorem frlmsubgval

Description: Subtraction in a free module. (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypotheses	frlmsubval.y	$$⊢Y=R\mathrm{freeLMod}I$$
	frlmsubval.b	$$⊢B={\mathrm{Base}}_Y$$
	frlmsubval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	frlmsubval.i	$$⊢\phi \to I\in W$$
	frlmsubval.f	$$⊢\phi \to F\in B$$
	frlmsubval.g	$$⊢\phi \to G\in B$$
	frlmsubval.a	$$⊢\underset{\dot{}}{-}={-}_R$$
	frlmsubval.p	$$⊢M={-}_Y$$
Assertion	frlmsubgval	$$⊢\phi \to FMG=F{\underset{\dot{}}{-}}_{f}G$$

Proof

Step	Hyp	Ref	Expression
1		frlmsubval.y	$$⊢Y=R\mathrm{freeLMod}I$$
2		frlmsubval.b	$$⊢B={\mathrm{Base}}_Y$$
3		frlmsubval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		frlmsubval.i	$$⊢\phi \to I\in W$$
5		frlmsubval.f	$$⊢\phi \to F\in B$$
6		frlmsubval.g	$$⊢\phi \to G\in B$$
7		frlmsubval.a	$$⊢\underset{\dot{}}{-}={-}_R$$
8		frlmsubval.p	$$⊢M={-}_Y$$
9	1 2	frlmpws	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
10	3 4 9	syl2anc	$$⊢\phi \to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
11	10	fveq2d	$$⊢\phi \to {-}_Y={-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
12	8 11	syl5eq	$$⊢\phi \to M={-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
13	12	oveqd	$$⊢\phi \to FMG=F{-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}G$$
14		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
15	3 14	syl	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
16		eqid	$$⊢\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I=\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I$$
17	16	pwslmod	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge I\in W\right)\to \mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\in \mathrm{LMod}$$
18	15 4 17	syl2anc	$$⊢\phi \to \mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\in \mathrm{LMod}$$
19		eqid	$$⊢\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
20	1 2 19	frlmlss	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to B\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
21	3 4 20	syl2anc	$$⊢\phi \to B\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
22	19	lsssubg	$$⊢\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\in \mathrm{LMod}\wedge B\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)\right)\to B\in \mathrm{SubGrp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
23	18 21 22	syl2anc	$$⊢\phi \to B\in \mathrm{SubGrp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
24		eqid	$$⊢{-}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={-}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
25		eqid	$$⊢\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
26		eqid	$$⊢{-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}={-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
27	24 25 26	subgsub	$$⊢\left(B\in \mathrm{SubGrp}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)\wedge F\in B\wedge G\in B\right)\to F{-}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}G=F{-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}G$$
28	23 5 6 27	syl3anc	$$⊢\phi \to F{-}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}G=F{-}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}G$$
29		lmodgrp	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{Grp}$$
30	3 14 29	3syl	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{Grp}$$
31		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
32	1 31 2	frlmbasmap	$$⊢\left(I\in W\wedge F\in B\right)\to F\in \left({{\mathrm{Base}}_R}^I\right)$$
33	4 5 32	syl2anc	$$⊢\phi \to F\in \left({{\mathrm{Base}}_R}^I\right)$$
34		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
35	16 34	pwsbas	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{Grp}\wedge I\in W\right)\to {{\mathrm{Base}}_R}^I={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
36	30 4 35	syl2anc	$$⊢\phi \to {{\mathrm{Base}}_R}^I={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
37	33 36	eleqtrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
38	1 31 2	frlmbasmap	$$⊢\left(I\in W\wedge G\in B\right)\to G\in \left({{\mathrm{Base}}_R}^I\right)$$
39	4 6 38	syl2anc	$$⊢\phi \to G\in \left({{\mathrm{Base}}_R}^I\right)$$
40	39 36	eleqtrd	$$⊢\phi \to G\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
41		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
42		rlmsub	$$⊢{-}_R={-}_{\mathrm{ringLMod}\left(R\right)}$$
43	7 42	eqtri	$$⊢\underset{\dot{}}{-}={-}_{\mathrm{ringLMod}\left(R\right)}$$
44	16 41 43 24	pwssub	$$⊢\left(\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{Grp}\wedge I\in W\right)\wedge \left(F\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}\wedge G\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}\right)\right)\to F{-}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}G=F{\underset{\dot{}}{-}}_{f}G$$
45	30 4 37 40 44	syl22anc	$$⊢\phi \to F{-}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}G=F{\underset{\dot{}}{-}}_{f}G$$
46	13 28 45	3eqtr2d	$$⊢\phi \to FMG=F{\underset{\dot{}}{-}}_{f}G$$