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