Theorem lindspropd

Description: Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023)

	Ref	Expression
Hypotheses	lindfpropd.1	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
	lindfpropd.2	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(L\right)}$$
	lindfpropd.3	$$⊢\phi \to 0_{\mathrm{Scalar}\left(K\right)}=0_{\mathrm{Scalar}\left(L\right)}$$
	lindfpropd.4	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	lindfpropd.5	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{\cdot }_{K}y\in {\mathrm{Base}}_K$$
	lindfpropd.6	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
	lindfpropd.k	$$⊢\phi \to K\in V$$
	lindfpropd.l	$$⊢\phi \to L\in W$$
Assertion	lindspropd	$$⊢\phi \to \mathrm{LIndS}\left(K\right)=\mathrm{LIndS}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		lindfpropd.1	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		lindfpropd.2	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(L\right)}$$
3		lindfpropd.3	$$⊢\phi \to 0_{\mathrm{Scalar}\left(K\right)}=0_{\mathrm{Scalar}\left(L\right)}$$
4		lindfpropd.4	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
5		lindfpropd.5	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{\cdot }_{K}y\in {\mathrm{Base}}_K$$
6		lindfpropd.6	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(K\right)}\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
7		lindfpropd.k	$$⊢\phi \to K\in V$$
8		lindfpropd.l	$$⊢\phi \to L\in W$$
9	1	sseq2d	$$⊢\phi \to \left(z\subseteq {\mathrm{Base}}_K\leftrightarrow z\subseteq {\mathrm{Base}}_L\right)$$
10		vex	$$⊢z\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to z\in \mathrm{V}$$
12	11	resiexd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_z\in \mathrm{V}$$
13	1 2 3 4 5 6 7 8 12	lindfpropd	$$⊢\phi \to \left(\left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}K\leftrightarrow \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}L\right)$$
14	9 13	anbi12d	$$⊢\phi \to \left(\left(z\subseteq {\mathrm{Base}}_K\wedge \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}K\right)\leftrightarrow \left(z\subseteq {\mathrm{Base}}_L\wedge \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}L\right)\right)$$
15		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
16	15	islinds	$$⊢K\in V\to \left(z\in \mathrm{LIndS}\left(K\right)\leftrightarrow \left(z\subseteq {\mathrm{Base}}_K\wedge \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}K\right)\right)$$
17	7 16	syl	$$⊢\phi \to \left(z\in \mathrm{LIndS}\left(K\right)\leftrightarrow \left(z\subseteq {\mathrm{Base}}_K\wedge \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}K\right)\right)$$
18		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
19	18	islinds	$$⊢L\in W\to \left(z\in \mathrm{LIndS}\left(L\right)\leftrightarrow \left(z\subseteq {\mathrm{Base}}_L\wedge \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}L\right)\right)$$
20	8 19	syl	$$⊢\phi \to \left(z\in \mathrm{LIndS}\left(L\right)\leftrightarrow \left(z\subseteq {\mathrm{Base}}_L\wedge \left({\mathrm{I}\upharpoonright }_z\right)\mathrm{LIndF}L\right)\right)$$
21	14 17 20	3bitr4d	$$⊢\phi \to \left(z\in \mathrm{LIndS}\left(K\right)\leftrightarrow z\in \mathrm{LIndS}\left(L\right)\right)$$
22	21	eqrdv	$$⊢\phi \to \mathrm{LIndS}\left(K\right)=\mathrm{LIndS}\left(L\right)$$