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	\|- ( ph -> B = ( Base ` K ) )
	dimpropd.b2	\|- ( ph -> B = ( Base ` L ) )
	dimpropd.w	\|- ( ph -> B C_ W )
	dimpropd.p	\|- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
	dimpropd.s1	\|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )
	dimpropd.s2	\|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
	dimpropd.f	\|- F = ( Scalar ` K )
	dimpropd.g	\|- G = ( Scalar ` L )
	dimpropd.p1	\|- ( ph -> P = ( Base ` F ) )
	dimpropd.p2	\|- ( ph -> P = ( Base ` G ) )
	dimpropd.a	\|- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
	dimpropd.v1	\|- ( ph -> K e. LVec )
	dimpropd.v2	\|- ( ph -> L e. LVec )
Assertion	dimpropd	\|- ( ph -> ( dim ` K ) = ( dim ` L ) )

Proof

Step	Hyp	Ref	Expression
1		dimpropd.b1	\|- ( ph -> B = ( Base ` K ) )
2		dimpropd.b2	\|- ( ph -> B = ( Base ` L ) )
3		dimpropd.w	\|- ( ph -> B C_ W )
4		dimpropd.p	\|- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
5		dimpropd.s1	\|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )
6		dimpropd.s2	\|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
7		dimpropd.f	\|- F = ( Scalar ` K )
8		dimpropd.g	\|- G = ( Scalar ` L )
9		dimpropd.p1	\|- ( ph -> P = ( Base ` F ) )
10		dimpropd.p2	\|- ( ph -> P = ( Base ` G ) )
11		dimpropd.a	\|- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
12		dimpropd.v1	\|- ( ph -> K e. LVec )
13		dimpropd.v2	\|- ( ph -> L e. LVec )
14		eqid	\|- ( LBasis ` K ) = ( LBasis ` K )
15	14	lbsex	\|- ( K e. LVec -> ( LBasis ` K ) =/= (/) )
16	12 15	syl	\|- ( ph -> ( LBasis ` K ) =/= (/) )
17		n0	\|- ( ( LBasis ` K ) =/= (/) <-> E. x x e. ( LBasis ` K ) )
18	16 17	sylib	\|- ( ph -> E. x x e. ( LBasis ` K ) )
19	14	dimval	\|- ( ( K e. LVec /\ x e. ( LBasis ` K ) ) -> ( dim ` K ) = ( # ` x ) )
20	12 19	sylan	\|- ( ( ph /\ x e. ( LBasis ` K ) ) -> ( dim ` K ) = ( # ` x ) )
21	1 2 3 4 5 6 7 8 9 10 11 12 13	lbspropd	\|- ( ph -> ( LBasis ` K ) = ( LBasis ` L ) )
22	21	eleq2d	\|- ( ph -> ( x e. ( LBasis ` K ) <-> x e. ( LBasis ` L ) ) )
23	22	biimpa	\|- ( ( ph /\ x e. ( LBasis ` K ) ) -> x e. ( LBasis ` L ) )
24		eqid	\|- ( LBasis ` L ) = ( LBasis ` L )
25	24	dimval	\|- ( ( L e. LVec /\ x e. ( LBasis ` L ) ) -> ( dim ` L ) = ( # ` x ) )
26	13 23 25	syl2an2r	\|- ( ( ph /\ x e. ( LBasis ` K ) ) -> ( dim ` L ) = ( # ` x ) )
27	20 26	eqtr4d	\|- ( ( ph /\ x e. ( LBasis ` K ) ) -> ( dim ` K ) = ( dim ` L ) )
28	18 27	exlimddv	\|- ( ph -> ( dim ` K ) = ( dim ` L ) )

Metamath Proof Explorer

Theorem dimpropd

Proof