Metamath Proof Explorer


Theorem lsmpropd

Description: If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015) (Revised by AV, 25-Apr-2024)

Ref Expression
Hypotheses lsmpropd.b1
|- ( ph -> B = ( Base ` K ) )
lsmpropd.b2
|- ( ph -> B = ( Base ` L ) )
lsmpropd.p
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lsmpropd.v1
|- ( ph -> K e. V )
lsmpropd.v2
|- ( ph -> L e. W )
Assertion lsmpropd
|- ( ph -> ( LSSum ` K ) = ( LSSum ` L ) )

Proof

Step Hyp Ref Expression
1 lsmpropd.b1
 |-  ( ph -> B = ( Base ` K ) )
2 lsmpropd.b2
 |-  ( ph -> B = ( Base ` L ) )
3 lsmpropd.p
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 lsmpropd.v1
 |-  ( ph -> K e. V )
5 lsmpropd.v2
 |-  ( ph -> L e. W )
6 simp11
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> ph )
7 simp12
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> t e. ~P B )
8 7 elpwid
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> t C_ B )
9 simp2
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> x e. t )
10 8 9 sseldd
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> x e. B )
11 simp13
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> u e. ~P B )
12 11 elpwid
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> u C_ B )
13 simp3
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> y e. u )
14 12 13 sseldd
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> y e. B )
15 6 10 14 3 syl12anc
 |-  ( ( ( ph /\ t e. ~P B /\ u e. ~P B ) /\ x e. t /\ y e. u ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
16 15 mpoeq3dva
 |-  ( ( ph /\ t e. ~P B /\ u e. ~P B ) -> ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) = ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) )
17 16 rneqd
 |-  ( ( ph /\ t e. ~P B /\ u e. ~P B ) -> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) = ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) )
18 17 mpoeq3dva
 |-  ( ph -> ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) )
19 1 pweqd
 |-  ( ph -> ~P B = ~P ( Base ` K ) )
20 mpoeq12
 |-  ( ( ~P B = ~P ( Base ` K ) /\ ~P B = ~P ( Base ` K ) ) -> ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) = ( t e. ~P ( Base ` K ) , u e. ~P ( Base ` K ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) )
21 19 19 20 syl2anc
 |-  ( ph -> ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) = ( t e. ~P ( Base ` K ) , u e. ~P ( Base ` K ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) )
22 2 pweqd
 |-  ( ph -> ~P B = ~P ( Base ` L ) )
23 mpoeq12
 |-  ( ( ~P B = ~P ( Base ` L ) /\ ~P B = ~P ( Base ` L ) ) -> ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) = ( t e. ~P ( Base ` L ) , u e. ~P ( Base ` L ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) )
24 22 22 23 syl2anc
 |-  ( ph -> ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) = ( t e. ~P ( Base ` L ) , u e. ~P ( Base ` L ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) )
25 18 21 24 3eqtr3d
 |-  ( ph -> ( t e. ~P ( Base ` K ) , u e. ~P ( Base ` K ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) = ( t e. ~P ( Base ` L ) , u e. ~P ( Base ` L ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) )
26 eqid
 |-  ( Base ` K ) = ( Base ` K )
27 eqid
 |-  ( +g ` K ) = ( +g ` K )
28 eqid
 |-  ( LSSum ` K ) = ( LSSum ` K )
29 26 27 28 lsmfval
 |-  ( K e. V -> ( LSSum ` K ) = ( t e. ~P ( Base ` K ) , u e. ~P ( Base ` K ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) )
30 4 29 syl
 |-  ( ph -> ( LSSum ` K ) = ( t e. ~P ( Base ` K ) , u e. ~P ( Base ` K ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` K ) y ) ) ) )
31 eqid
 |-  ( Base ` L ) = ( Base ` L )
32 eqid
 |-  ( +g ` L ) = ( +g ` L )
33 eqid
 |-  ( LSSum ` L ) = ( LSSum ` L )
34 31 32 33 lsmfval
 |-  ( L e. W -> ( LSSum ` L ) = ( t e. ~P ( Base ` L ) , u e. ~P ( Base ` L ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) )
35 5 34 syl
 |-  ( ph -> ( LSSum ` L ) = ( t e. ~P ( Base ` L ) , u e. ~P ( Base ` L ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` L ) y ) ) ) )
36 25 30 35 3eqtr4d
 |-  ( ph -> ( LSSum ` K ) = ( LSSum ` L ) )