| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ringrng 20283 | . . . . . 6
⊢ (𝑟 ∈ Ring → 𝑟 ∈ Rng) | 
| 2 | 1 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑟 ∈ Ring → 𝑟 ∈ Rng)) | 
| 3 | 2 | ssrdv 3988 | . . . 4
⊢ (𝜑 → Ring ⊆
Rng) | 
| 4 | 3 | ssrind 4243 | . . 3
⊢ (𝜑 → (Ring ∩ 𝑈) ⊆ (Rng ∩ 𝑈)) | 
| 5 |  | rhmsscrnghm.r | . . 3
⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) | 
| 6 |  | rhmsscrnghm.s | . . 3
⊢ (𝜑 → 𝑆 = (Rng ∩ 𝑈)) | 
| 7 | 4, 5, 6 | 3sstr4d 4038 | . 2
⊢ (𝜑 → 𝑅 ⊆ 𝑆) | 
| 8 |  | ovres 7600 | . . . . . . 7
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) = (𝑥 RingHom 𝑦)) | 
| 9 | 8 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) = (𝑥 RingHom 𝑦)) | 
| 10 | 9 | eleq2d 2826 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ↔ ℎ ∈ (𝑥 RingHom 𝑦))) | 
| 11 |  | rhmisrnghm 20481 | . . . . . 6
⊢ (ℎ ∈ (𝑥 RingHom 𝑦) → ℎ ∈ (𝑥 RngHom 𝑦)) | 
| 12 | 7 | sseld 3981 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑅 → 𝑥 ∈ 𝑆)) | 
| 13 | 7 | sseld 3981 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝑅 → 𝑦 ∈ 𝑆)) | 
| 14 | 12, 13 | anim12d 609 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆))) | 
| 15 | 14 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) | 
| 16 |  | ovres 7600 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦) = (𝑥 RngHom 𝑦)) | 
| 17 | 15, 16 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦) = (𝑥 RngHom 𝑦)) | 
| 18 | 17 | eleq2d 2826 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦) ↔ ℎ ∈ (𝑥 RngHom 𝑦))) | 
| 19 | 11, 18 | imbitrrid 246 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥 RingHom 𝑦) → ℎ ∈ (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦))) | 
| 20 | 10, 19 | sylbid 240 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) → ℎ ∈ (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦))) | 
| 21 | 20 | ssrdv 3988 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ⊆ (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦)) | 
| 22 | 21 | ralrimivva 3201 | . 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ⊆ (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦)) | 
| 23 |  | inss1 4236 | . . . . . 6
⊢ (Ring
∩ 𝑈) ⊆
Ring | 
| 24 | 5, 23 | eqsstrdi 4027 | . . . . 5
⊢ (𝜑 → 𝑅 ⊆ Ring) | 
| 25 |  | xpss12 5699 | . . . . 5
⊢ ((𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring) → (𝑅 × 𝑅) ⊆ (Ring ×
Ring)) | 
| 26 | 24, 24, 25 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑅 × 𝑅) ⊆ (Ring ×
Ring)) | 
| 27 |  | rhmfn 20500 | . . . . 5
⊢  RingHom
Fn (Ring × Ring) | 
| 28 |  | fnssresb 6689 | . . . . 5
⊢ ( RingHom
Fn (Ring × Ring) → (( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅) ↔ (𝑅 × 𝑅) ⊆ (Ring ×
Ring))) | 
| 29 | 27, 28 | mp1i 13 | . . . 4
⊢ (𝜑 → (( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅) ↔ (𝑅 × 𝑅) ⊆ (Ring ×
Ring))) | 
| 30 | 26, 29 | mpbird 257 | . . 3
⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅)) | 
| 31 |  | inss1 4236 | . . . . . 6
⊢ (Rng
∩ 𝑈) ⊆
Rng | 
| 32 | 6, 31 | eqsstrdi 4027 | . . . . 5
⊢ (𝜑 → 𝑆 ⊆ Rng) | 
| 33 |  | xpss12 5699 | . . . . 5
⊢ ((𝑆 ⊆ Rng ∧ 𝑆 ⊆ Rng) → (𝑆 × 𝑆) ⊆ (Rng ×
Rng)) | 
| 34 | 32, 32, 33 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑆 × 𝑆) ⊆ (Rng ×
Rng)) | 
| 35 |  | rnghmfn 20440 | . . . . 5
⊢  RngHom
Fn (Rng × Rng) | 
| 36 |  | fnssresb 6689 | . . . . 5
⊢ ( RngHom
Fn (Rng × Rng) → (( RngHom ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆) ↔ (𝑆 × 𝑆) ⊆ (Rng ×
Rng))) | 
| 37 | 35, 36 | mp1i 13 | . . . 4
⊢ (𝜑 → (( RngHom ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆) ↔ (𝑆 × 𝑆) ⊆ (Rng ×
Rng))) | 
| 38 | 34, 37 | mpbird 257 | . . 3
⊢ (𝜑 → ( RngHom ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆)) | 
| 39 |  | rhmsscrnghm.u | . . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) | 
| 40 |  | incom 4208 | . . . . . 6
⊢ (Rng
∩ 𝑈) = (𝑈 ∩ Rng) | 
| 41 |  | inex1g 5318 | . . . . . 6
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Rng) ∈ V) | 
| 42 | 40, 41 | eqeltrid 2844 | . . . . 5
⊢ (𝑈 ∈ 𝑉 → (Rng ∩ 𝑈) ∈ V) | 
| 43 | 39, 42 | syl 17 | . . . 4
⊢ (𝜑 → (Rng ∩ 𝑈) ∈ V) | 
| 44 | 6, 43 | eqeltrd 2840 | . . 3
⊢ (𝜑 → 𝑆 ∈ V) | 
| 45 | 30, 38, 44 | isssc 17865 | . 2
⊢ (𝜑 → (( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHom ↾
(𝑆 × 𝑆)) ↔ (𝑅 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ⊆ (𝑥( RngHom ↾ (𝑆 × 𝑆))𝑦)))) | 
| 46 | 7, 22, 45 | mpbir2and 713 | 1
⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHom ↾
(𝑆 × 𝑆))) |