Theorem tngdim

Description: Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypothesis	tnglvec.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
Assertion	tngdim	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( dim ‘ 𝐺 ) = ( dim ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		tnglvec.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		eqidd	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	1 3	tngbas	⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
5	4	adantl	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
6		ssidd	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝐺 ) )
7		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8	1 7	tngplusg	⊢ ( 𝑁 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
9	8	adantl	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
10	9	oveqdr	⊢ ( ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
11		lveclmod	⊢ ( 𝐺 ∈ LVec → 𝐺 ∈ LMod )
12		eqid	⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 )
13		eqid	⊢ ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝐺 )
14		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) )
15	3 12 13 14	lmodvscl	⊢ ( ( 𝐺 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
16	15	3expb	⊢ ( ( 𝐺 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
17	11 16	sylan	⊢ ( ( 𝐺 ∈ LVec ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
18	17	adantlr	⊢ ( ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
19	1 13	tngvsca	⊢ ( 𝑁 ∈ 𝑉 → ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑇 ) )
20	19	adantl	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑇 ) )
21	20	oveqdr	⊢ ( ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) 𝑦 ) )
22		eqid	⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
23		eqidd	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) ) )
24	1 12	tngsca	⊢ ( 𝑁 ∈ 𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
25	24	adantl	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
26	25	fveq2d	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
27	25	fveq2d	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( +g ‘ ( Scalar ‘ 𝐺 ) ) = ( +g ‘ ( Scalar ‘ 𝑇 ) ) )
28	27	oveqdr	⊢ ( ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ) ) → ( 𝑥 ( +g ‘ ( Scalar ‘ 𝐺 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( Scalar ‘ 𝑇 ) ) 𝑦 ) )
29		simpl	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → 𝐺 ∈ LVec )
30	1	tnglvec	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ LVec ↔ 𝑇 ∈ LVec ) )
31	30	biimpac	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → 𝑇 ∈ LVec )
32	2 5 6 10 18 21 12 22 23 26 28 29 31	dimpropd	⊢ ( ( 𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉 ) → ( dim ‘ 𝐺 ) = ( dim ‘ 𝑇 ) )