| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rhmqusspan.1 | . . 3
⊢  0 =
(0g‘𝐻) | 
| 2 |  | rhmqusspan.2 | . . 3
⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) | 
| 3 |  | rhmqusspan.3 | . . 3
⊢ 𝐾 = (◡𝐹 “ { 0 }) | 
| 4 |  | rhmqusspan.4 | . . 3
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) | 
| 5 |  | rhmqusspan.5 | . . 3
⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪
(𝐹 “ 𝑞)) | 
| 6 |  | rhmqusspan.6 | . . 3
⊢ (𝜑 → 𝐺 ∈ CRing) | 
| 7 |  | rhmqusspan.7 | . . . 4
⊢ 𝑁 = ((RSpan‘𝐺)‘{𝑋}) | 
| 8 | 6 | crngringd 20244 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ Ring) | 
| 9 |  | rhmqusspan.8 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺)) | 
| 10 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 11 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(RSpan‘𝐺) =
(RSpan‘𝐺) | 
| 12 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(∥r‘𝐺) = (∥r‘𝐺) | 
| 13 | 10, 11, 12 | rspsn 21344 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Ring ∧ 𝑋 ∈ (Base‘𝐺)) → ((RSpan‘𝐺)‘{𝑋}) = {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦}) | 
| 14 | 8, 9, 13 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((RSpan‘𝐺)‘{𝑋}) = {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦}) | 
| 15 | 14 | eleq2d 2826 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ((RSpan‘𝐺)‘{𝑋}) ↔ 𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦})) | 
| 16 | 15 | biimpd 229 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ((RSpan‘𝐺)‘{𝑋}) → 𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦})) | 
| 17 | 16 | imp 406 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → 𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦}) | 
| 18 |  | vex 3483 | . . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑥 ∈ V) | 
| 20 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝑋(∥r‘𝐺)𝑦 ↔ 𝑋(∥r‘𝐺)𝑥)) | 
| 21 | 20 | elabg 3675 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ V → (𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦} ↔ 𝑋(∥r‘𝐺)𝑥)) | 
| 22 | 21 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → (𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦} → 𝑋(∥r‘𝐺)𝑥)) | 
| 23 | 19, 22 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦} → 𝑋(∥r‘𝐺)𝑥)) | 
| 24 | 23 | imp 406 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦}) → 𝑋(∥r‘𝐺)𝑥) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(.r‘𝐺) = (.r‘𝐺) | 
| 26 | 10, 12, 25 | dvdsr 20363 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑋(∥r‘𝐺)𝑥 ↔ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) | 
| 27 | 26 | biimpi 216 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋(∥r‘𝐺)𝑥 → (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) | 
| 28 | 27 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋(∥r‘𝐺)𝑥) → (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) | 
| 29 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧(.r‘𝐺)𝑋) = 𝑥 → (𝐹‘(𝑧(.r‘𝐺)𝑋)) = (𝐹‘𝑥)) | 
| 30 | 29 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧(.r‘𝐺)𝑋) = 𝑥 → (𝐹‘𝑥) = (𝐹‘(𝑧(.r‘𝐺)𝑋))) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) ∧ (𝑧(.r‘𝐺)𝑋) = 𝑥) → (𝐹‘𝑥) = (𝐹‘(𝑧(.r‘𝐺)𝑋))) | 
| 32 | 2 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → 𝐹 ∈ (𝐺 RingHom 𝐻)) | 
| 33 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → 𝑧 ∈ (Base‘𝐺)) | 
| 34 | 9 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → 𝑋 ∈ (Base‘𝐺)) | 
| 35 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(.r‘𝐻) = (.r‘𝐻) | 
| 36 | 10, 25, 35 | rhmmul 20487 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (𝐺 RingHom 𝐻) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑋 ∈ (Base‘𝐺)) → (𝐹‘(𝑧(.r‘𝐺)𝑋)) = ((𝐹‘𝑧)(.r‘𝐻)(𝐹‘𝑋))) | 
| 37 | 32, 33, 34, 36 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝐹‘(𝑧(.r‘𝐺)𝑋)) = ((𝐹‘𝑧)(.r‘𝐻)(𝐹‘𝑋))) | 
| 38 |  | rhmqusspan.9 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐹‘𝑋) = 0 ) | 
| 39 | 38 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝐹‘𝑋) = 0 ) | 
| 40 | 39 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝐹‘𝑧)(.r‘𝐻)(𝐹‘𝑋)) = ((𝐹‘𝑧)(.r‘𝐻) 0 )) | 
| 41 |  | rhmrcl2 20478 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → 𝐻 ∈ Ring) | 
| 42 |  | ringsrg 20295 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐻 ∈ Ring → 𝐻 ∈ SRing) | 
| 43 | 32, 41, 42 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → 𝐻 ∈ SRing) | 
| 44 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 45 | 10, 44 | rhmf 20486 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) | 
| 46 | 2, 45 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) | 
| 48 | 47 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝐹‘𝑧) ∈ (Base‘𝐻)) | 
| 49 | 44, 35, 1 | srgrz 20205 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐻 ∈ SRing ∧ (𝐹‘𝑧) ∈ (Base‘𝐻)) → ((𝐹‘𝑧)(.r‘𝐻) 0 ) = 0 ) | 
| 50 | 43, 48, 49 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝐹‘𝑧)(.r‘𝐻) 0 ) = 0 ) | 
| 51 | 40, 50 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝐹‘𝑧)(.r‘𝐻)(𝐹‘𝑋)) = 0 ) | 
| 52 | 37, 51 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝐹‘(𝑧(.r‘𝐺)𝑋)) = 0 ) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) ∧ (𝑧(.r‘𝐺)𝑋) = 𝑥) → (𝐹‘(𝑧(.r‘𝐺)𝑋)) = 0 ) | 
| 54 | 31, 53 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) ∧ 𝑧 ∈ (Base‘𝐺)) ∧ (𝑧(.r‘𝐺)𝑋) = 𝑥) → (𝐹‘𝑥) = 0 ) | 
| 55 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧(𝑦(.r‘𝐺)𝑋) = 𝑥 | 
| 56 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑦(𝑧(.r‘𝐺)𝑋) = 𝑥 | 
| 57 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑧 → (𝑦(.r‘𝐺)𝑋) = (𝑧(.r‘𝐺)𝑋)) | 
| 58 | 57 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑧 → ((𝑦(.r‘𝐺)𝑋) = 𝑥 ↔ (𝑧(.r‘𝐺)𝑋) = 𝑥)) | 
| 59 | 55, 56, 58 | cbvrexw 3306 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑦 ∈
(Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥 ↔ ∃𝑧 ∈ (Base‘𝐺)(𝑧(.r‘𝐺)𝑋) = 𝑥) | 
| 60 | 59 | biimpi 216 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑦 ∈
(Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥 → ∃𝑧 ∈ (Base‘𝐺)(𝑧(.r‘𝐺)𝑋) = 𝑥) | 
| 61 | 60 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥) → ∃𝑧 ∈ (Base‘𝐺)(𝑧(.r‘𝐺)𝑋) = 𝑥) | 
| 62 | 61 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) → ∃𝑧 ∈ (Base‘𝐺)(𝑧(.r‘𝐺)𝑋) = 𝑥) | 
| 63 | 54, 62 | r19.29a 3161 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥)) → (𝐹‘𝑥) = 0 ) | 
| 64 | 63 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥) → (𝐹‘𝑥) = 0 )) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋(∥r‘𝐺)𝑥) → ((𝑋 ∈ (Base‘𝐺) ∧ ∃𝑦 ∈ (Base‘𝐺)(𝑦(.r‘𝐺)𝑋) = 𝑥) → (𝐹‘𝑥) = 0 )) | 
| 66 | 28, 65 | mpd 15 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋(∥r‘𝐺)𝑥) → (𝐹‘𝑥) = 0 ) | 
| 67 | 66 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋(∥r‘𝐺)𝑥 → (𝐹‘𝑥) = 0 )) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦}) → (𝑋(∥r‘𝐺)𝑥 → (𝐹‘𝑥) = 0 )) | 
| 69 | 24, 68 | mpd 15 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦}) → (𝐹‘𝑥) = 0 ) | 
| 70 | 69 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦} → (𝐹‘𝑥) = 0 )) | 
| 71 | 70 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → (𝑥 ∈ {𝑦 ∣ 𝑋(∥r‘𝐺)𝑦} → (𝐹‘𝑥) = 0 )) | 
| 72 | 17, 71 | mpd 15 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → (𝐹‘𝑥) = 0 ) | 
| 73 |  | fvexd 6920 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → (𝐹‘𝑥) ∈ V) | 
| 74 |  | elsng 4639 | . . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ V → ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )) | 
| 75 | 73, 74 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 )) | 
| 76 | 72, 75 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → (𝐹‘𝑥) ∈ { 0 }) | 
| 77 | 46 | ffund 6739 | . . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) | 
| 78 | 77 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → Fun 𝐹) | 
| 79 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(LIdeal‘𝐺) =
(LIdeal‘𝐺) | 
| 80 | 79, 10 | lidl1 21244 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ Ring →
(Base‘𝐺) ∈
(LIdeal‘𝐺)) | 
| 81 | 8, 80 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝐺) ∈ (LIdeal‘𝐺)) | 
| 82 | 9 | snssd 4808 | . . . . . . . . . . . 12
⊢ (𝜑 → {𝑋} ⊆ (Base‘𝐺)) | 
| 83 | 11, 79 | rspssp 21250 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ Ring ∧
(Base‘𝐺) ∈
(LIdeal‘𝐺) ∧
{𝑋} ⊆
(Base‘𝐺)) →
((RSpan‘𝐺)‘{𝑋}) ⊆ (Base‘𝐺)) | 
| 84 | 8, 81, 82, 83 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → ((RSpan‘𝐺)‘{𝑋}) ⊆ (Base‘𝐺)) | 
| 85 | 84 | sselda 3982 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → 𝑥 ∈ (Base‘𝐺)) | 
| 86 |  | fdm 6744 | . . . . . . . . . . . 12
⊢ (𝐹:(Base‘𝐺)⟶(Base‘𝐻) → dom 𝐹 = (Base‘𝐺)) | 
| 87 | 46, 86 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = (Base‘𝐺)) | 
| 88 | 87 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → dom 𝐹 = (Base‘𝐺)) | 
| 89 | 85, 88 | eleqtrrd 2843 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → 𝑥 ∈ dom 𝐹) | 
| 90 |  | fvimacnv 7072 | . . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) ∈ { 0 } ↔ 𝑥 ∈ (◡𝐹 “ { 0 }))) | 
| 91 | 78, 89, 90 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → ((𝐹‘𝑥) ∈ { 0 } ↔ 𝑥 ∈ (◡𝐹 “ { 0 }))) | 
| 92 | 76, 91 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((RSpan‘𝐺)‘{𝑋})) → 𝑥 ∈ (◡𝐹 “ { 0 })) | 
| 93 | 92 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((RSpan‘𝐺)‘{𝑋}) → 𝑥 ∈ (◡𝐹 “ { 0 }))) | 
| 94 | 93 | ssrdv 3988 | . . . . 5
⊢ (𝜑 → ((RSpan‘𝐺)‘{𝑋}) ⊆ (◡𝐹 “ { 0 })) | 
| 95 | 3 | eqcomi 2745 | . . . . 5
⊢ (◡𝐹 “ { 0 }) = 𝐾 | 
| 96 | 94, 95 | sseqtrdi 4023 | . . . 4
⊢ (𝜑 → ((RSpan‘𝐺)‘{𝑋}) ⊆ 𝐾) | 
| 97 | 7, 96 | eqsstrid 4021 | . . 3
⊢ (𝜑 → 𝑁 ⊆ 𝐾) | 
| 98 | 11, 10, 79 | rspcl 21246 | . . . . 5
⊢ ((𝐺 ∈ Ring ∧ {𝑋} ⊆ (Base‘𝐺)) → ((RSpan‘𝐺)‘{𝑋}) ∈ (LIdeal‘𝐺)) | 
| 99 | 8, 82, 98 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((RSpan‘𝐺)‘{𝑋}) ∈ (LIdeal‘𝐺)) | 
| 100 | 7, 99 | eqeltrid 2844 | . . 3
⊢ (𝜑 → 𝑁 ∈ (LIdeal‘𝐺)) | 
| 101 | 1, 2, 3, 4, 5, 6, 97, 100 | rhmqusnsg 21296 | . 2
⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐻)) | 
| 102 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝐺)) → 𝐹 ∈ (𝐺 RingHom 𝐻)) | 
| 103 |  | rhmghm 20485 | . . . . 5
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | 
| 104 | 102, 103 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝐺)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | 
| 105 | 97 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝐺)) → 𝑁 ⊆ 𝐾) | 
| 106 |  | lidlnsg 21259 | . . . . . 6
⊢ ((𝐺 ∈ Ring ∧ 𝑁 ∈ (LIdeal‘𝐺)) → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 107 | 8, 100, 106 | syl2anc 584 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 108 | 107 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝐺)) → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 109 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝐺)) → 𝑔 ∈ (Base‘𝐺)) | 
| 110 | 1, 104, 3, 4, 5, 105, 108, 109 | ghmqusnsglem1 19299 | . . 3
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘𝐺)) → (𝐽‘[𝑔](𝐺 ~QG 𝑁)) = (𝐹‘𝑔)) | 
| 111 | 110 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑔 ∈ (Base‘𝐺)(𝐽‘[𝑔](𝐺 ~QG 𝑁)) = (𝐹‘𝑔)) | 
| 112 | 101, 111 | jca 511 | 1
⊢ (𝜑 → (𝐽 ∈ (𝑄 RingHom 𝐻) ∧ ∀𝑔 ∈ (Base‘𝐺)(𝐽‘[𝑔](𝐺 ~QG 𝑁)) = (𝐹‘𝑔))) |