Theorem lsppropd

Description: If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015) (Revised by AV, 24-Apr-2024)

	Ref	Expression
Hypotheses	lsspropd.b1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	lsspropd.b2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	lsspropd.w	$$⊢\phi \to B\subseteq W$$
	lsspropd.p	$$⊢\left(\phi \wedge \left(x\in W\wedge y\in W\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	lsspropd.s1	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in B\right)\right)\to x{\cdot }_{K}y\in W$$
	lsspropd.s2	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
	lsspropd.p1	$$⊢\phi \to P={\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}$$
	lsspropd.p2	$$⊢\phi \to P={\mathrm{Base}}_{\mathrm{Scalar}\left(L\right)}$$
	lsppropd.v1	$$⊢\phi \to K\in X$$
	lsppropd.v2	$$⊢\phi \to L\in Y$$
Assertion	lsppropd	$$⊢\phi \to \mathrm{LSpan}\left(K\right)=\mathrm{LSpan}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsspropd.b1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		lsspropd.b2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		lsspropd.w	$$⊢\phi \to B\subseteq W$$
4		lsspropd.p	$$⊢\left(\phi \wedge \left(x\in W\wedge y\in W\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
5		lsspropd.s1	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in B\right)\right)\to x{\cdot }_{K}y\in W$$
6		lsspropd.s2	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
7		lsspropd.p1	$$⊢\phi \to P={\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}$$
8		lsspropd.p2	$$⊢\phi \to P={\mathrm{Base}}_{\mathrm{Scalar}\left(L\right)}$$
9		lsppropd.v1	$$⊢\phi \to K\in X$$
10		lsppropd.v2	$$⊢\phi \to L\in Y$$
11	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
12	11	pweqd	$$⊢\phi \to 𝒫{\mathrm{Base}}_K=𝒫{\mathrm{Base}}_L$$
13	1 2 3 4 5 6 7 8	lsspropd	$$⊢\phi \to \mathrm{LSubSp}\left(K\right)=\mathrm{LSubSp}\left(L\right)$$
14	13	rabeqdv	$$⊢\phi \to \left\{t\in \mathrm{LSubSp}\left(K\right)|s\subseteq t\right\}=\left\{t\in \mathrm{LSubSp}\left(L\right)|s\subseteq t\right\}$$
15	14	inteqd	$$⊢\phi \to \bigcap \left\{t\in \mathrm{LSubSp}\left(K\right)|s\subseteq t\right\}=\bigcap \left\{t\in \mathrm{LSubSp}\left(L\right)|s\subseteq t\right\}$$
16	12 15	mpteq12dv	$$⊢\phi \to \left(s\in 𝒫{\mathrm{Base}}_K⟼\bigcap \left\{t\in \mathrm{LSubSp}\left(K\right)|s\subseteq t\right\}\right)=\left(s\in 𝒫{\mathrm{Base}}_L⟼\bigcap \left\{t\in \mathrm{LSubSp}\left(L\right)|s\subseteq t\right\}\right)$$
17		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
18		eqid	$$⊢\mathrm{LSubSp}\left(K\right)=\mathrm{LSubSp}\left(K\right)$$
19		eqid	$$⊢\mathrm{LSpan}\left(K\right)=\mathrm{LSpan}\left(K\right)$$
20	17 18 19	lspfval	$$⊢K\in X\to \mathrm{LSpan}\left(K\right)=\left(s\in 𝒫{\mathrm{Base}}_K⟼\bigcap \left\{t\in \mathrm{LSubSp}\left(K\right)|s\subseteq t\right\}\right)$$
21	9 20	syl	$$⊢\phi \to \mathrm{LSpan}\left(K\right)=\left(s\in 𝒫{\mathrm{Base}}_K⟼\bigcap \left\{t\in \mathrm{LSubSp}\left(K\right)|s\subseteq t\right\}\right)$$
22		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
23		eqid	$$⊢\mathrm{LSubSp}\left(L\right)=\mathrm{LSubSp}\left(L\right)$$
24		eqid	$$⊢\mathrm{LSpan}\left(L\right)=\mathrm{LSpan}\left(L\right)$$
25	22 23 24	lspfval	$$⊢L\in Y\to \mathrm{LSpan}\left(L\right)=\left(s\in 𝒫{\mathrm{Base}}_L⟼\bigcap \left\{t\in \mathrm{LSubSp}\left(L\right)|s\subseteq t\right\}\right)$$
26	10 25	syl	$$⊢\phi \to \mathrm{LSpan}\left(L\right)=\left(s\in 𝒫{\mathrm{Base}}_L⟼\bigcap \left\{t\in \mathrm{LSubSp}\left(L\right)|s\subseteq t\right\}\right)$$
27	16 21 26	3eqtr4d	$$⊢\phi \to \mathrm{LSpan}\left(K\right)=\mathrm{LSpan}\left(L\right)$$