Metamath Proof Explorer

Theorem lbspropd

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

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

Proof

Step Hyp Ref Expression
1 lbspropd.b1 
 |-  ( ph -> B = ( Base ` K ) )
2 lbspropd.b2 
 |-  ( ph -> B = ( Base ` L ) )
3 lbspropd.w 
 |-  ( ph -> B C_ W )
4 lbspropd.p 
 |-  ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
5 lbspropd.s1 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )
6 lbspropd.s2 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
7 lbspropd.f 
 |-  F = ( Scalar ` K )
8 lbspropd.g 
 |-  G = ( Scalar ` L )
9 lbspropd.p1 
 |-  ( ph -> P = ( Base ` F ) )
10 lbspropd.p2 
 |-  ( ph -> P = ( Base ` G ) )
11 lbspropd.a 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
12 lbspropd.v1 
 |-  ( ph -> K e. X )
13 lbspropd.v2 
 |-  ( ph -> L e. Y )
14 simplll 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> ph )
15 eldifi 
 |-  ( v e. ( P \ { ( 0g ` F ) } ) -> v e. P )
16 15 adantl 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> v e. P )
17 simpr 
 |-  ( ( ph /\ z C_ B ) -> z C_ B )
18 17 sselda 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> u e. B )
19 18 adantr 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> u e. B )
20 6 oveqrspc2v 
 |-  ( ( ph /\ ( v e. P /\ u e. B ) ) -> ( v ( .s ` K ) u ) = ( v ( .s ` L ) u ) )
21 14 16 19 20 syl12anc 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> ( v ( .s ` K ) u ) = ( v ( .s ` L ) u ) )
22 7 fveq2i 
 |-  ( Base ` F ) = ( Base ` ( Scalar ` K ) )
23 9 22 eqtrdi 
 |-  ( ph -> P = ( Base ` ( Scalar ` K ) ) )
24 8 fveq2i 
 |-  ( Base ` G ) = ( Base ` ( Scalar ` L ) )
25 10 24 eqtrdi 
 |-  ( ph -> P = ( Base ` ( Scalar ` L ) ) )
26 1 2 3 4 5 6 23 25 12 13 lsppropd 
 |-  ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )
27 14 26 syl 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> ( LSpan ` K ) = ( LSpan ` L ) )
28 27 fveq1d 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> ( ( LSpan ` K ) ` ( z \ { u } ) ) = ( ( LSpan ` L ) ` ( z \ { u } ) ) )
29 21 28 eleq12d 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> ( ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) <-> ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) )
30 29 notbid 
 |-  ( ( ( ( ph /\ z C_ B ) /\ u e. z ) /\ v e. ( P \ { ( 0g ` F ) } ) ) -> ( -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) <-> -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) )
31 30 ralbidva 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( A. v e. ( P \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) <-> A. v e. ( P \ { ( 0g ` F ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) )
32 9 ad2antrr 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> P = ( Base ` F ) )
33 32 difeq1d 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( P \ { ( 0g ` F ) } ) = ( ( Base ` F ) \ { ( 0g ` F ) } ) )
34 33 raleqdv 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( A. v e. ( P \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) <-> A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) )
35 10 ad2antrr 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> P = ( Base ` G ) )
36 9 10 11 grpidpropd 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` G ) )
37 36 ad2antrr 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( 0g ` F ) = ( 0g ` G ) )
38 37 sneqd 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> { ( 0g ` F ) } = { ( 0g ` G ) } )
39 35 38 difeq12d 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( P \ { ( 0g ` F ) } ) = ( ( Base ` G ) \ { ( 0g ` G ) } ) )
40 39 raleqdv 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( A. v e. ( P \ { ( 0g ` F ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) <-> A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) )
41 31 34 40 3bitr3d 
 |-  ( ( ( ph /\ z C_ B ) /\ u e. z ) -> ( A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) <-> A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) )
42 41 ralbidva 
 |-  ( ( ph /\ z C_ B ) -> ( A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) <-> A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) )
43 42 anbi2d 
 |-  ( ( ph /\ z C_ B ) -> ( ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) <-> ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) )
44 43 pm5.32da 
 |-  ( ph -> ( ( z C_ B /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) <-> ( z C_ B /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) ) )
45 1 sseq2d 
 |-  ( ph -> ( z C_ B <-> z C_ ( Base ` K ) ) )
46 45 anbi1d 
 |-  ( ph -> ( ( z C_ B /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) <-> ( z C_ ( Base ` K ) /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) ) )
47 2 sseq2d 
 |-  ( ph -> ( z C_ B <-> z C_ ( Base ` L ) ) )
48 26 fveq1d 
 |-  ( ph -> ( ( LSpan ` K ) ` z ) = ( ( LSpan ` L ) ` z ) )
49 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
50 48 49 eqeq12d 
 |-  ( ph -> ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) <-> ( ( LSpan ` L ) ` z ) = ( Base ` L ) ) )
51 50 anbi1d 
 |-  ( ph -> ( ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) <-> ( ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) )
52 47 51 anbi12d 
 |-  ( ph -> ( ( z C_ B /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) <-> ( z C_ ( Base ` L ) /\ ( ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) ) )
53 44 46 52 3bitr3d 
 |-  ( ph -> ( ( z C_ ( Base ` K ) /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) <-> ( z C_ ( Base ` L ) /\ ( ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) ) )
54 3anass 
 |-  ( ( z C_ ( Base ` K ) /\ ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) <-> ( z C_ ( Base ` K ) /\ ( ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) )
55 3anass 
 |-  ( ( z C_ ( Base ` L ) /\ ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) <-> ( z C_ ( Base ` L ) /\ ( ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) )
56 53 54 55 3bitr4g 
 |-  ( ph -> ( ( z C_ ( Base ` K ) /\ ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) <-> ( z C_ ( Base ` L ) /\ ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) )
57 eqid 
 |-  ( Base ` K ) = ( Base ` K )
58 eqid 
 |-  ( .s ` K ) = ( .s ` K )
59 eqid 
 |-  ( Base ` F ) = ( Base ` F )
60 eqid 
 |-  ( LBasis ` K ) = ( LBasis ` K )
61 eqid 
 |-  ( LSpan ` K ) = ( LSpan ` K )
62 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
63 57 7 58 59 60 61 62 islbs 
 |-  ( K e. X -> ( z e. ( LBasis ` K ) <-> ( z C_ ( Base ` K ) /\ ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) )
64 12 63 syl 
 |-  ( ph -> ( z e. ( LBasis ` K ) <-> ( z C_ ( Base ` K ) /\ ( ( LSpan ` K ) ` z ) = ( Base ` K ) /\ A. u e. z A. v e. ( ( Base ` F ) \ { ( 0g ` F ) } ) -. ( v ( .s ` K ) u ) e. ( ( LSpan ` K ) ` ( z \ { u } ) ) ) ) )
65 eqid 
 |-  ( Base ` L ) = ( Base ` L )
66 eqid 
 |-  ( .s ` L ) = ( .s ` L )
67 eqid 
 |-  ( Base ` G ) = ( Base ` G )
68 eqid 
 |-  ( LBasis ` L ) = ( LBasis ` L )
69 eqid 
 |-  ( LSpan ` L ) = ( LSpan ` L )
70 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
71 65 8 66 67 68 69 70 islbs 
 |-  ( L e. Y -> ( z e. ( LBasis ` L ) <-> ( z C_ ( Base ` L ) /\ ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) )
72 13 71 syl 
 |-  ( ph -> ( z e. ( LBasis ` L ) <-> ( z C_ ( Base ` L ) /\ ( ( LSpan ` L ) ` z ) = ( Base ` L ) /\ A. u e. z A. v e. ( ( Base ` G ) \ { ( 0g ` G ) } ) -. ( v ( .s ` L ) u ) e. ( ( LSpan ` L ) ` ( z \ { u } ) ) ) ) )
73 56 64 72 3bitr4d 
 |-  ( ph -> ( z e. ( LBasis ` K ) <-> z e. ( LBasis ` L ) ) )
74 73 eqrdv 
 |-  ( ph -> ( LBasis ` K ) = ( LBasis ` L ) )