Metamath Proof Explorer

Theorem ngppropd

Description: Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses ngppropd.1 
|- ( ph -> B = ( Base ` K ) )
ngppropd.2 
|- ( ph -> B = ( Base ` L ) )
ngppropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
ngppropd.4 
|- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
ngppropd.5 
|- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
Assertion ngppropd 
|- ( ph -> ( K e. NrmGrp <-> L e. NrmGrp ) )

Proof

Step Hyp Ref Expression
1 ngppropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 ngppropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 ngppropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 ngppropd.4 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
5 ngppropd.5 
 |-  ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
6 1 2 4 5 mspropd 
 |-  ( ph -> ( K e. MetSp <-> L e. MetSp ) )
7 6 adantr 
 |-  ( ( ph /\ K e. Grp ) -> ( K e. MetSp <-> L e. MetSp ) )
8 1 adantr 
 |-  ( ( ph /\ K e. Grp ) -> B = ( Base ` K ) )
9 2 adantr 
 |-  ( ( ph /\ K e. Grp ) -> B = ( Base ` L ) )
10 simpr 
 |-  ( ( ph /\ K e. Grp ) -> K e. Grp )
11 3 adantlr 
 |-  ( ( ( ph /\ K e. Grp ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
12 4 adantr 
 |-  ( ( ph /\ K e. Grp ) -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
13 8 9 10 11 12 nmpropd2 
 |-  ( ( ph /\ K e. Grp ) -> ( norm ` K ) = ( norm ` L ) )
14 8 9 10 11 grpsubpropd2 
 |-  ( ( ph /\ K e. Grp ) -> ( -g ` K ) = ( -g ` L ) )
15 13 14 coeq12d 
 |-  ( ( ph /\ K e. Grp ) -> ( ( norm ` K ) o. ( -g ` K ) ) = ( ( norm ` L ) o. ( -g ` L ) ) )
16 1 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` K ) X. ( Base ` K ) ) )
17 16 reseq2d 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
18 2 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` L ) X. ( Base ` L ) ) )
19 18 reseq2d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
20 4 17 19 3eqtr3d 
 |-  ( ph -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
21 20 adantr 
 |-  ( ( ph /\ K e. Grp ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
22 15 21 eqeq12d 
 |-  ( ( ph /\ K e. Grp ) -> ( ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) <-> ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) )
23 7 22 anbi12d 
 |-  ( ( ph /\ K e. Grp ) -> ( ( K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) <-> ( L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) )
24 23 pm5.32da 
 |-  ( ph -> ( ( K e. Grp /\ ( K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) ) <-> ( K e. Grp /\ ( L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) ) )
25 1 2 3 grppropd 
 |-  ( ph -> ( K e. Grp <-> L e. Grp ) )
26 25 anbi1d 
 |-  ( ph -> ( ( K e. Grp /\ ( L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) <-> ( L e. Grp /\ ( L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) ) )
27 24 26 bitrd 
 |-  ( ph -> ( ( K e. Grp /\ ( K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) ) <-> ( L e. Grp /\ ( L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) ) )
28 3anass 
 |-  ( ( K e. Grp /\ K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) <-> ( K e. Grp /\ ( K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) ) )
29 3anass 
 |-  ( ( L e. Grp /\ L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) <-> ( L e. Grp /\ ( L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) )
30 27 28 29 3bitr4g 
 |-  ( ph -> ( ( K e. Grp /\ K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) <-> ( L e. Grp /\ L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) ) )
31 eqid 
 |-  ( norm ` K ) = ( norm ` K )
32 eqid 
 |-  ( -g ` K ) = ( -g ` K )
33 eqid 
 |-  ( dist ` K ) = ( dist ` K )
34 eqid 
 |-  ( Base ` K ) = ( Base ` K )
35 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
36 31 32 33 34 35 isngp2 
 |-  ( K e. NrmGrp <-> ( K e. Grp /\ K e. MetSp /\ ( ( norm ` K ) o. ( -g ` K ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
37 eqid 
 |-  ( norm ` L ) = ( norm ` L )
38 eqid 
 |-  ( -g ` L ) = ( -g ` L )
39 eqid 
 |-  ( dist ` L ) = ( dist ` L )
40 eqid 
 |-  ( Base ` L ) = ( Base ` L )
41 eqid 
 |-  ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) )
42 37 38 39 40 41 isngp2 
 |-  ( L e. NrmGrp <-> ( L e. Grp /\ L e. MetSp /\ ( ( norm ` L ) o. ( -g ` L ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ) )
43 30 36 42 3bitr4g 
 |-  ( ph -> ( K e. NrmGrp <-> L e. NrmGrp ) )