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 ⊢ 𝐴 = ( Base ‘ 𝑅 )
gim0to0ALT.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
gim0to0ALT.n ⊢ 𝑁 = ( 0g ‘ 𝑆 )
gim0to0ALT.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion f1rhm0to0ALT ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 gim0to0ALT.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
2 gim0to0ALT.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 gim0to0ALT.n ⊢ 𝑁 = ( 0g ‘ 𝑆 )
4 gim0to0ALT.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
7 1 2 4 3 ghmf1 ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = 𝑁 → 𝑥 = 0 ) ) )
8 6 7 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = 𝑁 → 𝑥 = 0 ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
10 9 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = 𝑁 ↔ ( 𝐹 ‘ 𝑋 ) = 𝑁 ) )
11 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
12 10 11 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑁 → 𝑥 = 0 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) ) )
13 12 rspcv ⊢ ( 𝑋 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = 𝑁 → 𝑥 = 0 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) ) )
14 13 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = 𝑁 → 𝑥 = 0 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) ) )
15 8 14 sylbid ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) ) )
16 15 ex ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑋 ∈ 𝐴 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) ) ) )
17 16 com23 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑋 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) ) ) )
18 17 3imp ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 → 𝑋 = 0 ) )
19 fveq2 ⊢ ( 𝑋 = 0 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 0 ) )
20 4 3 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 0 ) = 𝑁 )
21 5 20 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ 0 ) = 𝑁 )
22 21 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 0 ) = 𝑁 )
23 19 22 sylan9eqr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 0 ) → ( 𝐹 ‘ 𝑋 ) = 𝑁 )
24 23 ex ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = 0 → ( 𝐹 ‘ 𝑋 ) = 𝑁 ) )
25 18 24 impbid ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )