Metamath Proof Explorer

Theorem isnsg2

Description: Weaken the condition of isnsg to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses isnsg.1 
|- X = ( Base ` G )
isnsg.2 
|- .+ = ( +g ` G )
Assertion isnsg2 
|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )

Proof

Step Hyp Ref Expression
1 isnsg.1 
 |-  X = ( Base ` G )
2 isnsg.2 
 |-  .+ = ( +g ` G )
3 1 2 isnsg 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) ) )
4 dfbi2 
 |-  ( ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> ( ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) )
5 4 ralbii 
 |-  ( A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> A. z e. X ( ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) )
6 5 ralbii 
 |-  ( A. x e. X A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> A. x e. X A. z e. X ( ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) )
7 r19.26-2 
 |-  ( A. x e. X A. z e. X ( ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) <-> ( A. x e. X A. z e. X ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ A. x e. X A. z e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) )
8 6 7 bitri 
 |-  ( A. x e. X A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> ( A. x e. X A. z e. X ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ A. x e. X A. z e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) )
9 oveq2 
 |-  ( z = y -> ( x .+ z ) = ( x .+ y ) )
10 9 eleq1d 
 |-  ( z = y -> ( ( x .+ z ) e. S <-> ( x .+ y ) e. S ) )
11 oveq1 
 |-  ( z = y -> ( z .+ x ) = ( y .+ x ) )
12 11 eleq1d 
 |-  ( z = y -> ( ( z .+ x ) e. S <-> ( y .+ x ) e. S ) )
13 10 12 imbi12d 
 |-  ( z = y -> ( ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) <-> ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )
14 13 cbvralvw 
 |-  ( A. z e. X ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) <-> A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) )
15 14 ralbii 
 |-  ( A. x e. X A. z e. X ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) )
16 ralcom 
 |-  ( A. x e. X A. z e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) <-> A. z e. X A. x e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) )
17 oveq2 
 |-  ( x = y -> ( z .+ x ) = ( z .+ y ) )
18 17 eleq1d 
 |-  ( x = y -> ( ( z .+ x ) e. S <-> ( z .+ y ) e. S ) )
19 oveq1 
 |-  ( x = y -> ( x .+ z ) = ( y .+ z ) )
20 19 eleq1d 
 |-  ( x = y -> ( ( x .+ z ) e. S <-> ( y .+ z ) e. S ) )
21 18 20 imbi12d 
 |-  ( x = y -> ( ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) <-> ( ( z .+ y ) e. S -> ( y .+ z ) e. S ) ) )
22 21 cbvralvw 
 |-  ( A. x e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) <-> A. y e. X ( ( z .+ y ) e. S -> ( y .+ z ) e. S ) )
23 22 ralbii 
 |-  ( A. z e. X A. x e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) <-> A. z e. X A. y e. X ( ( z .+ y ) e. S -> ( y .+ z ) e. S ) )
24 oveq1 
 |-  ( z = x -> ( z .+ y ) = ( x .+ y ) )
25 24 eleq1d 
 |-  ( z = x -> ( ( z .+ y ) e. S <-> ( x .+ y ) e. S ) )
26 oveq2 
 |-  ( z = x -> ( y .+ z ) = ( y .+ x ) )
27 26 eleq1d 
 |-  ( z = x -> ( ( y .+ z ) e. S <-> ( y .+ x ) e. S ) )
28 25 27 imbi12d 
 |-  ( z = x -> ( ( ( z .+ y ) e. S -> ( y .+ z ) e. S ) <-> ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )
29 28 ralbidv 
 |-  ( z = x -> ( A. y e. X ( ( z .+ y ) e. S -> ( y .+ z ) e. S ) <-> A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )
30 29 cbvralvw 
 |-  ( A. z e. X A. y e. X ( ( z .+ y ) e. S -> ( y .+ z ) e. S ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) )
31 16 23 30 3bitri 
 |-  ( A. x e. X A. z e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) )
32 15 31 anbi12i 
 |-  ( ( A. x e. X A. z e. X ( ( x .+ z ) e. S -> ( z .+ x ) e. S ) /\ A. x e. X A. z e. X ( ( z .+ x ) e. S -> ( x .+ z ) e. S ) ) <-> ( A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )
33 anidm 
 |-  ( ( A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) )
34 8 32 33 3bitri 
 |-  ( A. x e. X A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) )
35 34 anbi2i 
 |-  ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )
36 3 35 bitri 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )