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 ) )