Theorem 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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	dimpropd.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	dimpropd.w	⊢ ( 𝜑 → 𝐵 ⊆ 𝑊 )
	dimpropd.p	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	dimpropd.s1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
	dimpropd.s2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
	dimpropd.f	⊢ 𝐹 = ( Scalar ‘ 𝐾 )
	dimpropd.g	⊢ 𝐺 = ( Scalar ‘ 𝐿 )
	dimpropd.p1	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
	dimpropd.p2	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
	dimpropd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
	dimpropd.v1	⊢ ( 𝜑 → 𝐾 ∈ LVec )
	dimpropd.v2	⊢ ( 𝜑 → 𝐿 ∈ LVec )
Assertion	dimpropd	⊢ ( 𝜑 → ( dim ‘ 𝐾 ) = ( dim ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		dimpropd.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		dimpropd.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		dimpropd.w	⊢ ( 𝜑 → 𝐵 ⊆ 𝑊 )
4		dimpropd.p	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
5		dimpropd.s1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝑊 )
6		dimpropd.s2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
7		dimpropd.f	⊢ 𝐹 = ( Scalar ‘ 𝐾 )
8		dimpropd.g	⊢ 𝐺 = ( Scalar ‘ 𝐿 )
9		dimpropd.p1	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
10		dimpropd.p2	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
11		dimpropd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
12		dimpropd.v1	⊢ ( 𝜑 → 𝐾 ∈ LVec )
13		dimpropd.v2	⊢ ( 𝜑 → 𝐿 ∈ LVec )
14		eqid	⊢ ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐾 )
15	14	lbsex	⊢ ( 𝐾 ∈ LVec → ( LBasis ‘ 𝐾 ) ≠ ∅ )
16	12 15	syl	⊢ ( 𝜑 → ( LBasis ‘ 𝐾 ) ≠ ∅ )
17		n0	⊢ ( ( LBasis ‘ 𝐾 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( LBasis ‘ 𝐾 ) )
18	16 17	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ ( LBasis ‘ 𝐾 ) )
19	14	dimval	⊢ ( ( 𝐾 ∈ LVec ∧ 𝑥 ∈ ( LBasis ‘ 𝐾 ) ) → ( dim ‘ 𝐾 ) = ( ♯ ‘ 𝑥 ) )
20	12 19	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LBasis ‘ 𝐾 ) ) → ( dim ‘ 𝐾 ) = ( ♯ ‘ 𝑥 ) )
21	1 2 3 4 5 6 7 8 9 10 11 12 13	lbspropd	⊢ ( 𝜑 → ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐿 ) )
22	21	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( LBasis ‘ 𝐾 ) ↔ 𝑥 ∈ ( LBasis ‘ 𝐿 ) ) )
23	22	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑥 ∈ ( LBasis ‘ 𝐿 ) )
24		eqid	⊢ ( LBasis ‘ 𝐿 ) = ( LBasis ‘ 𝐿 )
25	24	dimval	⊢ ( ( 𝐿 ∈ LVec ∧ 𝑥 ∈ ( LBasis ‘ 𝐿 ) ) → ( dim ‘ 𝐿 ) = ( ♯ ‘ 𝑥 ) )
26	13 23 25	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LBasis ‘ 𝐾 ) ) → ( dim ‘ 𝐿 ) = ( ♯ ‘ 𝑥 ) )
27	20 26	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LBasis ‘ 𝐾 ) ) → ( dim ‘ 𝐾 ) = ( dim ‘ 𝐿 ) )
28	18 27	exlimddv	⊢ ( 𝜑 → ( dim ‘ 𝐾 ) = ( dim ‘ 𝐿 ) )