Theorem lidlrsppropd

Description: The left ideals and ring span of a ring depend only on the ring components. Here W is expected to be either B (when closure is available) or _V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	lidlpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	lidlpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	lidlpropd.3	$$⊢\phi \to B\subseteq W$$
	lidlpropd.4	$$⊢\left(\phi \wedge \left(x\in W\wedge y\in W\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	lidlpropd.5	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y\in W$$
	lidlpropd.6	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	lidlrsppropd	$$⊢\phi \to \left(\mathrm{LIdeal}\left(K\right)=\mathrm{LIdeal}\left(L\right)\wedge \mathrm{RSpan}\left(K\right)=\mathrm{RSpan}\left(L\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lidlpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		lidlpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		lidlpropd.3	$$⊢\phi \to B\subseteq W$$
4		lidlpropd.4	$$⊢\left(\phi \wedge \left(x\in W\wedge y\in W\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
5		lidlpropd.5	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y\in W$$
6		lidlpropd.6	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
7		rlmbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{ringLMod}\left(K\right)}$$
8	1 7	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{ringLMod}\left(K\right)}$$
9		rlmbas	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_{\mathrm{ringLMod}\left(L\right)}$$
10	2 9	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{ringLMod}\left(L\right)}$$
11		rlmplusg	$$⊢{+}_K={+}_{\mathrm{ringLMod}\left(K\right)}$$
12	11	oveqi	$$⊢x{+}_{K}y=x{+}_{\mathrm{ringLMod}\left(K\right)}y$$
13		rlmplusg	$$⊢{+}_L={+}_{\mathrm{ringLMod}\left(L\right)}$$
14	13	oveqi	$$⊢x{+}_{L}y=x{+}_{\mathrm{ringLMod}\left(L\right)}y$$
15	4 12 14	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in W\wedge y\in W\right)\right)\to x{+}_{\mathrm{ringLMod}\left(K\right)}y=x{+}_{\mathrm{ringLMod}\left(L\right)}y$$
16		rlmvsca	$$⊢{\cdot }_K={\cdot }_{\mathrm{ringLMod}\left(K\right)}$$
17	16	oveqi	$$⊢x{\cdot }_{K}y=x{\cdot }_{\mathrm{ringLMod}\left(K\right)}y$$
18	17 5	eqeltrrid	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{\mathrm{ringLMod}\left(K\right)}y\in W$$
19		rlmvsca	$$⊢{\cdot }_L={\cdot }_{\mathrm{ringLMod}\left(L\right)}$$
20	19	oveqi	$$⊢x{\cdot }_{L}y=x{\cdot }_{\mathrm{ringLMod}\left(L\right)}y$$
21	6 17 20	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{\mathrm{ringLMod}\left(K\right)}y=x{\cdot }_{\mathrm{ringLMod}\left(L\right)}y$$
22		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
23		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
24	22 23	strfvi	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{I}\left(K\right)}$$
25		rlmsca2	$$⊢\mathrm{I}\left(K\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(K\right)\right)$$
26	25	fveq2i	$$⊢{\mathrm{Base}}_{\mathrm{I}\left(K\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(K\right)\right)}$$
27	24 26	eqtri	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(K\right)\right)}$$
28	1 27	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(K\right)\right)}$$
29		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
30	22 29	strfvi	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_{\mathrm{I}\left(L\right)}$$
31		rlmsca2	$$⊢\mathrm{I}\left(L\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(L\right)\right)$$
32	31	fveq2i	$$⊢{\mathrm{Base}}_{\mathrm{I}\left(L\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(L\right)\right)}$$
33	30 32	eqtri	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(L\right)\right)}$$
34	2 33	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(L\right)\right)}$$
35	8 10 3 15 18 21 28 34	lsspropd	$$⊢\phi \to \mathrm{LSubSp}\left(\mathrm{ringLMod}\left(K\right)\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(L\right)\right)$$
36		lidlval	$$⊢\mathrm{LIdeal}\left(K\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(K\right)\right)$$
37		lidlval	$$⊢\mathrm{LIdeal}\left(L\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(L\right)\right)$$
38	35 36 37	3eqtr4g	$$⊢\phi \to \mathrm{LIdeal}\left(K\right)=\mathrm{LIdeal}\left(L\right)$$
39		fvexd	$$⊢\phi \to \mathrm{ringLMod}\left(K\right)\in \mathrm{V}$$
40		fvexd	$$⊢\phi \to \mathrm{ringLMod}\left(L\right)\in \mathrm{V}$$
41	8 10 3 15 18 21 28 34 39 40	lsppropd	$$⊢\phi \to \mathrm{LSpan}\left(\mathrm{ringLMod}\left(K\right)\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(L\right)\right)$$
42		rspval	$$⊢\mathrm{RSpan}\left(K\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(K\right)\right)$$
43		rspval	$$⊢\mathrm{RSpan}\left(L\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(L\right)\right)$$
44	41 42 43	3eqtr4g	$$⊢\phi \to \mathrm{RSpan}\left(K\right)=\mathrm{RSpan}\left(L\right)$$
45	38 44	jca	$$⊢\phi \to \left(\mathrm{LIdeal}\left(K\right)=\mathrm{LIdeal}\left(L\right)\wedge \mathrm{RSpan}\left(K\right)=\mathrm{RSpan}\left(L\right)\right)$$