Proof of Theorem rhmunitinv
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rhmrcl1 20477 | . . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) | 
| 2 |  | eqid 2736 | . . . . . . 7
⊢
(Unit‘𝑅) =
(Unit‘𝑅) | 
| 3 |  | eqid 2736 | . . . . . . 7
⊢
(invr‘𝑅) = (invr‘𝑅) | 
| 4 |  | eqid 2736 | . . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 5 |  | eqid 2736 | . . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 6 | 2, 3, 4, 5 | unitlinv 20394 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ (Unit‘𝑅)) →
(((invr‘𝑅)‘𝐴)(.r‘𝑅)𝐴) = (1r‘𝑅)) | 
| 7 | 1, 6 | sylan 580 | . . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (((invr‘𝑅)‘𝐴)(.r‘𝑅)𝐴) = (1r‘𝑅)) | 
| 8 | 7 | fveq2d 6909 | . . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘(((invr‘𝑅)‘𝐴)(.r‘𝑅)𝐴)) = (𝐹‘(1r‘𝑅))) | 
| 9 |  | simpl 482 | . . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 10 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 11 | 10, 2 | unitss 20377 | . . . . . 6
⊢
(Unit‘𝑅)
⊆ (Base‘𝑅) | 
| 12 | 2, 3 | unitinvcl 20391 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ (Unit‘𝑅)) →
((invr‘𝑅)‘𝐴) ∈ (Unit‘𝑅)) | 
| 13 | 1, 12 | sylan 580 | . . . . . 6
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((invr‘𝑅)‘𝐴) ∈ (Unit‘𝑅)) | 
| 14 | 11, 13 | sselid 3980 | . . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((invr‘𝑅)‘𝐴) ∈ (Base‘𝑅)) | 
| 15 |  | simpr 484 | . . . . . 6
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐴 ∈ (Unit‘𝑅)) | 
| 16 | 11, 15 | sselid 3980 | . . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐴 ∈ (Base‘𝑅)) | 
| 17 |  | eqid 2736 | . . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) | 
| 18 | 10, 4, 17 | rhmmul 20487 | . . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((invr‘𝑅)‘𝐴) ∈ (Base‘𝑅) ∧ 𝐴 ∈ (Base‘𝑅)) → (𝐹‘(((invr‘𝑅)‘𝐴)(.r‘𝑅)𝐴)) = ((𝐹‘((invr‘𝑅)‘𝐴))(.r‘𝑆)(𝐹‘𝐴))) | 
| 19 | 9, 14, 16, 18 | syl3anc 1372 | . . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘(((invr‘𝑅)‘𝐴)(.r‘𝑅)𝐴)) = ((𝐹‘((invr‘𝑅)‘𝐴))(.r‘𝑆)(𝐹‘𝐴))) | 
| 20 |  | eqid 2736 | . . . . . 6
⊢
(1r‘𝑆) = (1r‘𝑆) | 
| 21 | 5, 20 | rhm1 20490 | . . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) | 
| 22 | 21 | adantr 480 | . . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) | 
| 23 | 8, 19, 22 | 3eqtr3d 2784 | . . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((𝐹‘((invr‘𝑅)‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) = (1r‘𝑆)) | 
| 24 |  | rhmrcl2 20478 | . . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) | 
| 25 | 24 | adantr 480 | . . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝑆 ∈ Ring) | 
| 26 |  | elrhmunit 20511 | . . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴) ∈ (Unit‘𝑆)) | 
| 27 |  | eqid 2736 | . . . . 5
⊢
(Unit‘𝑆) =
(Unit‘𝑆) | 
| 28 |  | eqid 2736 | . . . . 5
⊢
(invr‘𝑆) = (invr‘𝑆) | 
| 29 | 27, 28, 17, 20 | unitlinv 20394 | . . . 4
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝐴) ∈ (Unit‘𝑆)) → (((invr‘𝑆)‘(𝐹‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) = (1r‘𝑆)) | 
| 30 | 25, 26, 29 | syl2anc 584 | . . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (((invr‘𝑆)‘(𝐹‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) = (1r‘𝑆)) | 
| 31 | 23, 30 | eqtr4d 2779 | . 2
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((𝐹‘((invr‘𝑅)‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) = (((invr‘𝑆)‘(𝐹‘𝐴))(.r‘𝑆)(𝐹‘𝐴))) | 
| 32 |  | eqid 2736 | . . . . . 6
⊢
((mulGrp‘𝑆)
↾s (Unit‘𝑆)) = ((mulGrp‘𝑆) ↾s (Unit‘𝑆)) | 
| 33 | 27, 32 | unitgrp 20384 | . . . . 5
⊢ (𝑆 ∈ Ring →
((mulGrp‘𝑆)
↾s (Unit‘𝑆)) ∈ Grp) | 
| 34 | 24, 33 | syl 17 | . . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((mulGrp‘𝑆) ↾s (Unit‘𝑆)) ∈ Grp) | 
| 35 | 34 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((mulGrp‘𝑆) ↾s (Unit‘𝑆)) ∈ Grp) | 
| 36 |  | elrhmunit 20511 | . . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ((invr‘𝑅)‘𝐴) ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) ∈ (Unit‘𝑆)) | 
| 37 | 13, 36 | syldan 591 | . . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) ∈ (Unit‘𝑆)) | 
| 38 | 27, 28 | unitinvcl 20391 | . . . 4
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝐴) ∈ (Unit‘𝑆)) → ((invr‘𝑆)‘(𝐹‘𝐴)) ∈ (Unit‘𝑆)) | 
| 39 | 25, 26, 38 | syl2anc 584 | . . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((invr‘𝑆)‘(𝐹‘𝐴)) ∈ (Unit‘𝑆)) | 
| 40 | 27, 32 | unitgrpbas 20383 | . . . 4
⊢
(Unit‘𝑆) =
(Base‘((mulGrp‘𝑆) ↾s (Unit‘𝑆))) | 
| 41 |  | fvex 6918 | . . . . 5
⊢
(Unit‘𝑆)
∈ V | 
| 42 |  | eqid 2736 | . . . . . . 7
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) | 
| 43 | 42, 17 | mgpplusg 20142 | . . . . . 6
⊢
(.r‘𝑆) = (+g‘(mulGrp‘𝑆)) | 
| 44 | 32, 43 | ressplusg 17335 | . . . . 5
⊢
((Unit‘𝑆)
∈ V → (.r‘𝑆) =
(+g‘((mulGrp‘𝑆) ↾s (Unit‘𝑆)))) | 
| 45 | 41, 44 | ax-mp 5 | . . . 4
⊢
(.r‘𝑆) =
(+g‘((mulGrp‘𝑆) ↾s (Unit‘𝑆))) | 
| 46 | 40, 45 | grprcan 18992 | . . 3
⊢
((((mulGrp‘𝑆)
↾s (Unit‘𝑆)) ∈ Grp ∧ ((𝐹‘((invr‘𝑅)‘𝐴)) ∈ (Unit‘𝑆) ∧ ((invr‘𝑆)‘(𝐹‘𝐴)) ∈ (Unit‘𝑆) ∧ (𝐹‘𝐴) ∈ (Unit‘𝑆))) → (((𝐹‘((invr‘𝑅)‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) = (((invr‘𝑆)‘(𝐹‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) ↔ (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴)))) | 
| 47 | 35, 37, 39, 26, 46 | syl13anc 1373 | . 2
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (((𝐹‘((invr‘𝑅)‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) = (((invr‘𝑆)‘(𝐹‘𝐴))(.r‘𝑆)(𝐹‘𝐴)) ↔ (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴)))) | 
| 48 | 31, 47 | mpbid 232 | 1
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴))) |