Metamath Proof Explorer

Theorem lsspropd

Description: If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015)

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 ) ) )
Assertion lsspropd 
|- ( ph -> ( LSubSp ` K ) = ( LSubSp ` 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 simpll 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ph )
10 simprl 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> z e. P )
11 simplr 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> s C_ B )
12 simprrl 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> a e. s )
13 11 12 sseldd 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> a e. B )
14 5 ralrimivva 
 |-  ( ph -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. W )
15 14 ad2antrr 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. W )
16 ovrspc2v 
 |-  ( ( ( z e. P /\ a e. B ) /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. W ) -> ( z ( .s ` K ) a ) e. W )
17 10 13 15 16 syl21anc 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ( z ( .s ` K ) a ) e. W )
18 3 ad2antrr 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> B C_ W )
19 simprrr 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> b e. s )
20 11 19 sseldd 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> b e. B )
21 18 20 sseldd 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> b e. W )
22 4 oveqrspc2v 
 |-  ( ( ph /\ ( ( z ( .s ` K ) a ) e. W /\ b e. W ) ) -> ( ( z ( .s ` K ) a ) ( +g ` K ) b ) = ( ( z ( .s ` K ) a ) ( +g ` L ) b ) )
23 9 17 21 22 syl12anc 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ( ( z ( .s ` K ) a ) ( +g ` K ) b ) = ( ( z ( .s ` K ) a ) ( +g ` L ) b ) )
24 6 oveqrspc2v 
 |-  ( ( ph /\ ( z e. P /\ a e. B ) ) -> ( z ( .s ` K ) a ) = ( z ( .s ` L ) a ) )
25 9 10 13 24 syl12anc 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ( z ( .s ` K ) a ) = ( z ( .s ` L ) a ) )
26 25 oveq1d 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ( ( z ( .s ` K ) a ) ( +g ` L ) b ) = ( ( z ( .s ` L ) a ) ( +g ` L ) b ) )
27 23 26 eqtrd 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ( ( z ( .s ` K ) a ) ( +g ` K ) b ) = ( ( z ( .s ` L ) a ) ( +g ` L ) b ) )
28 27 eleq1d 
 |-  ( ( ( ph /\ s C_ B ) /\ ( z e. P /\ ( a e. s /\ b e. s ) ) ) -> ( ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s <-> ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) )
29 28 anassrs 
 |-  ( ( ( ( ph /\ s C_ B ) /\ z e. P ) /\ ( a e. s /\ b e. s ) ) -> ( ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s <-> ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) )
30 29 2ralbidva 
 |-  ( ( ( ph /\ s C_ B ) /\ z e. P ) -> ( A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s <-> A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) )
31 30 ralbidva 
 |-  ( ( ph /\ s C_ B ) -> ( A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s <-> A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) )
32 31 anbi2d 
 |-  ( ( ph /\ s C_ B ) -> ( ( s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) <-> ( s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) ) )
33 32 pm5.32da 
 |-  ( ph -> ( ( s C_ B /\ ( s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) ) <-> ( s C_ B /\ ( s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) ) ) )
34 3anass 
 |-  ( ( s C_ B /\ s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) <-> ( s C_ B /\ ( s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) ) )
35 3anass 
 |-  ( ( s C_ B /\ s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) <-> ( s C_ B /\ ( s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) ) )
36 33 34 35 3bitr4g 
 |-  ( ph -> ( ( s C_ B /\ s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) <-> ( s C_ B /\ s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) ) )
37 1 sseq2d 
 |-  ( ph -> ( s C_ B <-> s C_ ( Base ` K ) ) )
38 7 raleqdv 
 |-  ( ph -> ( A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s <-> A. z e. ( Base ` ( Scalar ` K ) ) A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) )
39 37 38 3anbi13d 
 |-  ( ph -> ( ( s C_ B /\ s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) <-> ( s C_ ( Base ` K ) /\ s =/= (/) /\ A. z e. ( Base ` ( Scalar ` K ) ) A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) ) )
40 2 sseq2d 
 |-  ( ph -> ( s C_ B <-> s C_ ( Base ` L ) ) )
41 8 raleqdv 
 |-  ( ph -> ( A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s <-> A. z e. ( Base ` ( Scalar ` L ) ) A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) )
42 40 41 3anbi13d 
 |-  ( ph -> ( ( s C_ B /\ s =/= (/) /\ A. z e. P A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) <-> ( s C_ ( Base ` L ) /\ s =/= (/) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) ) )
43 36 39 42 3bitr3d 
 |-  ( ph -> ( ( s C_ ( Base ` K ) /\ s =/= (/) /\ A. z e. ( Base ` ( Scalar ` K ) ) A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) <-> ( s C_ ( Base ` L ) /\ s =/= (/) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) ) )
44 eqid 
 |-  ( Scalar ` K ) = ( Scalar ` K )
45 eqid 
 |-  ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` K ) )
46 eqid 
 |-  ( Base ` K ) = ( Base ` K )
47 eqid 
 |-  ( +g ` K ) = ( +g ` K )
48 eqid 
 |-  ( .s ` K ) = ( .s ` K )
49 eqid 
 |-  ( LSubSp ` K ) = ( LSubSp ` K )
50 44 45 46 47 48 49 islss 
 |-  ( s e. ( LSubSp ` K ) <-> ( s C_ ( Base ` K ) /\ s =/= (/) /\ A. z e. ( Base ` ( Scalar ` K ) ) A. a e. s A. b e. s ( ( z ( .s ` K ) a ) ( +g ` K ) b ) e. s ) )
51 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
52 eqid 
 |-  ( Base ` ( Scalar ` L ) ) = ( Base ` ( Scalar ` L ) )
53 eqid 
 |-  ( Base ` L ) = ( Base ` L )
54 eqid 
 |-  ( +g ` L ) = ( +g ` L )
55 eqid 
 |-  ( .s ` L ) = ( .s ` L )
56 eqid 
 |-  ( LSubSp ` L ) = ( LSubSp ` L )
57 51 52 53 54 55 56 islss 
 |-  ( s e. ( LSubSp ` L ) <-> ( s C_ ( Base ` L ) /\ s =/= (/) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. a e. s A. b e. s ( ( z ( .s ` L ) a ) ( +g ` L ) b ) e. s ) )
58 43 50 57 3bitr4g 
 |-  ( ph -> ( s e. ( LSubSp ` K ) <-> s e. ( LSubSp ` L ) ) )
59 58 eqrdv 
 |-  ( ph -> ( LSubSp ` K ) = ( LSubSp ` L ) )