dimpropd

Description: If two structures have the same components (properties), they have the same dimension. (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Hypotheses	dimpropd.b1	$⊢ φ \to B = {Base}_{K}$
	dimpropd.b2	$⊢ φ \to B = {Base}_{L}$
	dimpropd.w	$⊢ φ \to B \subseteq W$
	dimpropd.p	$⊢ (φ \land (x \in W \land y \in W)) \to x +_{K} y = x +_{L} y$
	dimpropd.s1	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y \in W$
	dimpropd.s2	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	dimpropd.f	$⊢ F = Scalar (K)$
	dimpropd.g	$⊢ G = Scalar (L)$
	dimpropd.p1	$⊢ φ \to P = {Base}_{F}$
	dimpropd.p2	$⊢ φ \to P = {Base}_{G}$
	dimpropd.a	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{F} y = x +_{G} y$
	dimpropd.v1	$⊢ φ \to K \in LVec$
	dimpropd.v2	$⊢ φ \to L \in LVec$
Assertion	dimpropd	$⊢ φ \to \dim (K) = \dim (L)$

Proof

Step	Hyp	Ref	Expression
1		dimpropd.b1	$⊢ φ \to B = {Base}_{K}$
2		dimpropd.b2	$⊢ φ \to B = {Base}_{L}$
3		dimpropd.w	$⊢ φ \to B \subseteq W$
4		dimpropd.p	$⊢ (φ \land (x \in W \land y \in W)) \to x +_{K} y = x +_{L} y$
5		dimpropd.s1	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y \in W$
6		dimpropd.s2	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
7		dimpropd.f	$⊢ F = Scalar (K)$
8		dimpropd.g	$⊢ G = Scalar (L)$
9		dimpropd.p1	$⊢ φ \to P = {Base}_{F}$
10		dimpropd.p2	$⊢ φ \to P = {Base}_{G}$
11		dimpropd.a	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{F} y = x +_{G} y$
12		dimpropd.v1	$⊢ φ \to K \in LVec$
13		dimpropd.v2	$⊢ φ \to L \in LVec$
14		eqid	$⊢ LBasis (K) = LBasis (K)$
15	14	lbsex	$⊢ K \in LVec \to LBasis (K) \neq \emptyset$
16	12 15	syl	$⊢ φ \to LBasis (K) \neq \emptyset$
17		n0	$⊢ LBasis (K) \neq \emptyset \leftrightarrow \exists x x \in LBasis (K)$
18	16 17	sylib	$⊢ φ \to \exists x x \in LBasis (K)$
19	14	dimval	$⊢ (K \in LVec \land x \in LBasis (K)) \to \dim (K) = \|x\|$
20	12 19	sylan	$⊢ (φ \land x \in LBasis (K)) \to \dim (K) = \|x\|$
21	1 2 3 4 5 6 7 8 9 10 11 12 13	lbspropd	$⊢ φ \to LBasis (K) = LBasis (L)$
22	21	eleq2d	$⊢ φ \to (x \in LBasis (K) \leftrightarrow x \in LBasis (L))$
23	22	biimpa	$⊢ (φ \land x \in LBasis (K)) \to x \in LBasis (L)$
24		eqid	$⊢ LBasis (L) = LBasis (L)$
25	24	dimval	$⊢ (L \in LVec \land x \in LBasis (L)) \to \dim (L) = \|x\|$
26	13 23 25	syl2an2r	$⊢ (φ \land x \in LBasis (K)) \to \dim (L) = \|x\|$
27	20 26	eqtr4d	$⊢ (φ \land x \in LBasis (K)) \to \dim (K) = \dim (L)$
28	18 27	exlimddv	$⊢ φ \to \dim (K) = \dim (L)$

Metamath Proof Explorer

Theorem dimpropd

Proof