Metamath Proof Explorer


Theorem lsppropd

Description: If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015) (Revised by AV, 24-Apr-2024)

Ref Expression
Hypotheses lsspropd.b1
|- ( ph -> B = ( Base ` K ) )
lsspropd.b2
|- ( ph -> B = ( Base ` L ) )
lsspropd.w
|- ( ph -> B C_ W )
lsspropd.p
|- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lsspropd.s1
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )
lsspropd.s2
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
lsspropd.p1
|- ( ph -> P = ( Base ` ( Scalar ` K ) ) )
lsspropd.p2
|- ( ph -> P = ( Base ` ( Scalar ` L ) ) )
lsppropd.v1
|- ( ph -> K e. X )
lsppropd.v2
|- ( ph -> L e. Y )
Assertion lsppropd
|- ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )

Proof

Step Hyp Ref Expression
1 lsspropd.b1
 |-  ( ph -> B = ( Base ` K ) )
2 lsspropd.b2
 |-  ( ph -> B = ( Base ` L ) )
3 lsspropd.w
 |-  ( ph -> B C_ W )
4 lsspropd.p
 |-  ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
5 lsspropd.s1
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )
6 lsspropd.s2
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
7 lsspropd.p1
 |-  ( ph -> P = ( Base ` ( Scalar ` K ) ) )
8 lsspropd.p2
 |-  ( ph -> P = ( Base ` ( Scalar ` L ) ) )
9 lsppropd.v1
 |-  ( ph -> K e. X )
10 lsppropd.v2
 |-  ( ph -> L e. Y )
11 1 2 eqtr3d
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
12 11 pweqd
 |-  ( ph -> ~P ( Base ` K ) = ~P ( Base ` L ) )
13 1 2 3 4 5 6 7 8 lsspropd
 |-  ( ph -> ( LSubSp ` K ) = ( LSubSp ` L ) )
14 13 rabeqdv
 |-  ( ph -> { t e. ( LSubSp ` K ) | s C_ t } = { t e. ( LSubSp ` L ) | s C_ t } )
15 14 inteqd
 |-  ( ph -> |^| { t e. ( LSubSp ` K ) | s C_ t } = |^| { t e. ( LSubSp ` L ) | s C_ t } )
16 12 15 mpteq12dv
 |-  ( ph -> ( s e. ~P ( Base ` K ) |-> |^| { t e. ( LSubSp ` K ) | s C_ t } ) = ( s e. ~P ( Base ` L ) |-> |^| { t e. ( LSubSp ` L ) | s C_ t } ) )
17 eqid
 |-  ( Base ` K ) = ( Base ` K )
18 eqid
 |-  ( LSubSp ` K ) = ( LSubSp ` K )
19 eqid
 |-  ( LSpan ` K ) = ( LSpan ` K )
20 17 18 19 lspfval
 |-  ( K e. X -> ( LSpan ` K ) = ( s e. ~P ( Base ` K ) |-> |^| { t e. ( LSubSp ` K ) | s C_ t } ) )
21 9 20 syl
 |-  ( ph -> ( LSpan ` K ) = ( s e. ~P ( Base ` K ) |-> |^| { t e. ( LSubSp ` K ) | s C_ t } ) )
22 eqid
 |-  ( Base ` L ) = ( Base ` L )
23 eqid
 |-  ( LSubSp ` L ) = ( LSubSp ` L )
24 eqid
 |-  ( LSpan ` L ) = ( LSpan ` L )
25 22 23 24 lspfval
 |-  ( L e. Y -> ( LSpan ` L ) = ( s e. ~P ( Base ` L ) |-> |^| { t e. ( LSubSp ` L ) | s C_ t } ) )
26 10 25 syl
 |-  ( ph -> ( LSpan ` L ) = ( s e. ~P ( Base ` L ) |-> |^| { t e. ( LSubSp ` L ) | s C_ t } ) )
27 16 21 26 3eqtr4d
 |-  ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )