Metamath Proof Explorer

Theorem f1rhm0to0ALT

Description: Alternate proof for f1ghm0to0 . Using ghmf1 does not make the proof shorter and requires disjoint variable restrictions! (Contributed by AV, 24-Oct-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses gim0to0ALT.a 
|- A = ( Base ` R )
gim0to0ALT.b 
|- B = ( Base ` S )
gim0to0ALT.n 
|- N = ( 0g ` S )
gim0to0ALT.0 
|- .0. = ( 0g ` R )
Assertion f1rhm0to0ALT 
|- ( ( F e. ( R RingHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )

Proof

Step Hyp Ref Expression
1 gim0to0ALT.a 
 |-  A = ( Base ` R )
2 gim0to0ALT.b 
 |-  B = ( Base ` S )
3 gim0to0ALT.n 
 |-  N = ( 0g ` S )
4 gim0to0ALT.0 
 |-  .0. = ( 0g ` R )
5 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
6 5 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ X e. A ) -> F e. ( R GrpHom S ) )
7 1 2 4 3 ghmf1 
 |-  ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> A. x e. A ( ( F ` x ) = N -> x = .0. ) ) )
8 6 7 syl 
 |-  ( ( F e. ( R RingHom S ) /\ X e. A ) -> ( F : A -1-1-> B <-> A. x e. A ( ( F ` x ) = N -> x = .0. ) ) )
9 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
10 9 eqeq1d 
 |-  ( x = X -> ( ( F ` x ) = N <-> ( F ` X ) = N ) )
11 eqeq1 
 |-  ( x = X -> ( x = .0. <-> X = .0. ) )
12 10 11 imbi12d 
 |-  ( x = X -> ( ( ( F ` x ) = N -> x = .0. ) <-> ( ( F ` X ) = N -> X = .0. ) ) )
13 12 rspcv 
 |-  ( X e. A -> ( A. x e. A ( ( F ` x ) = N -> x = .0. ) -> ( ( F ` X ) = N -> X = .0. ) ) )
14 13 adantl 
 |-  ( ( F e. ( R RingHom S ) /\ X e. A ) -> ( A. x e. A ( ( F ` x ) = N -> x = .0. ) -> ( ( F ` X ) = N -> X = .0. ) ) )
15 8 14 sylbid 
 |-  ( ( F e. ( R RingHom S ) /\ X e. A ) -> ( F : A -1-1-> B -> ( ( F ` X ) = N -> X = .0. ) ) )
16 15 ex 
 |-  ( F e. ( R RingHom S ) -> ( X e. A -> ( F : A -1-1-> B -> ( ( F ` X ) = N -> X = .0. ) ) ) )
17 16 com23 
 |-  ( F e. ( R RingHom S ) -> ( F : A -1-1-> B -> ( X e. A -> ( ( F ` X ) = N -> X = .0. ) ) ) )
18 17 3imp 
 |-  ( ( F e. ( R RingHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N -> X = .0. ) )
19 fveq2 
 |-  ( X = .0. -> ( F ` X ) = ( F ` .0. ) )
20 4 3 ghmid 
 |-  ( F e. ( R GrpHom S ) -> ( F ` .0. ) = N )
21 5 20 syl 
 |-  ( F e. ( R RingHom S ) -> ( F ` .0. ) = N )
22 21 3ad2ant1 
 |-  ( ( F e. ( R RingHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( F ` .0. ) = N )
23 19 22 sylan9eqr 
 |-  ( ( ( F e. ( R RingHom S ) /\ F : A -1-1-> B /\ X e. A ) /\ X = .0. ) -> ( F ` X ) = N )
24 23 ex 
 |-  ( ( F e. ( R RingHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( X = .0. -> ( F ` X ) = N ) )
25 18 24 impbid 
 |-  ( ( F e. ( R RingHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )