| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rng2idlring.b | . 2
⊢ 𝐵 = (Base‘𝑅) | 
| 2 |  | eqid 2736 | . 2
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 3 |  | eqid 2736 | . 2
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 4 |  | eqid 2736 | . 2
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 5 |  | rng2idlring.r | . . 3
⊢ (𝜑 → 𝑅 ∈ Rng) | 
| 6 |  | rnggrp 20156 | . . 3
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) | 
| 7 | 5, 6 | syl 17 | . 2
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 8 |  | rng2idlring.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) | 
| 9 |  | rng2idlring.j | . . . 4
⊢ 𝐽 = (𝑅 ↾s 𝐼) | 
| 10 |  | rng2idlring.u | . . . 4
⊢ (𝜑 → 𝐽 ∈ Ring) | 
| 11 |  | rng2idlring.t | . . . 4
⊢  · =
(.r‘𝑅) | 
| 12 |  | rng2idlring.1 | . . . 4
⊢  1 =
(1r‘𝐽) | 
| 13 |  | rngqiprngim.g | . . . 4
⊢  ∼ =
(𝑅 ~QG
𝐼) | 
| 14 |  | rngqiprngim.q | . . . 4
⊢ 𝑄 = (𝑅 /s ∼ ) | 
| 15 |  | rngqiprngim.c | . . . 4
⊢ 𝐶 = (Base‘𝑄) | 
| 16 |  | rngqiprngim.p | . . . 4
⊢ 𝑃 = (𝑄 ×s 𝐽) | 
| 17 | 5, 8, 9, 10, 1, 11, 12, 13, 14, 15, 16 | rngqiprng 21307 | . . 3
⊢ (𝜑 → 𝑃 ∈ Rng) | 
| 18 |  | rnggrp 20156 | . . 3
⊢ (𝑃 ∈ Rng → 𝑃 ∈ Grp) | 
| 19 | 17, 18 | syl 17 | . 2
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 20 |  | rngqiprngim.f | . . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈[𝑥] ∼ , ( 1 · 𝑥)〉) | 
| 21 | 5, 8, 9, 10, 1, 11, 12, 13, 14, 15, 16, 20 | rngqiprngimf 21308 | . . 3
⊢ (𝜑 → 𝐹:𝐵⟶(𝐶 × 𝐼)) | 
| 22 | 5, 8, 9, 10, 1, 11, 12, 13, 14, 15, 16 | rngqipbas 21306 | . . . 4
⊢ (𝜑 → (Base‘𝑃) = (𝐶 × 𝐼)) | 
| 23 | 22 | feq3d 6722 | . . 3
⊢ (𝜑 → (𝐹:𝐵⟶(Base‘𝑃) ↔ 𝐹:𝐵⟶(𝐶 × 𝐼))) | 
| 24 | 21, 23 | mpbird 257 | . 2
⊢ (𝜑 → 𝐹:𝐵⟶(Base‘𝑃)) | 
| 25 |  | ringrng 20283 | . . . . . . . . 9
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) | 
| 26 | 10, 25 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Rng) | 
| 27 | 9, 26 | eqeltrrid 2845 | . . . . . . 7
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) | 
| 28 | 5, 8, 27 | rng2idlnsg 21277 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) | 
| 29 | 28, 1, 13, 14 | ecqusaddd 19211 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → [(𝑎(+g‘𝑅)𝑏)] ∼ = ([𝑎] ∼
(+g‘𝑄)[𝑏] ∼ )) | 
| 30 | 5, 8, 9, 10, 1, 11, 12 | rngqiprngghmlem3 21300 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( 1 · (𝑎(+g‘𝑅)𝑏)) = (( 1 · 𝑎)(+g‘𝐽)( 1 · 𝑏))) | 
| 31 | 29, 30 | opeq12d 4880 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 〈[(𝑎(+g‘𝑅)𝑏)] ∼ , ( 1 · (𝑎(+g‘𝑅)𝑏))〉 = 〈([𝑎] ∼
(+g‘𝑄)[𝑏] ∼ ), (( 1 · 𝑎)(+g‘𝐽)( 1 · 𝑏))〉) | 
| 32 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 33 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝐽) =
(Base‘𝐽) | 
| 34 | 14 | ovexi 7466 | . . . . . 6
⊢ 𝑄 ∈ V | 
| 35 | 34 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑄 ∈ V) | 
| 36 | 10 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐽 ∈ Ring) | 
| 37 |  | simpl 482 | . . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ 𝐵) | 
| 38 | 13, 14, 1, 32 | quseccl0 19204 | . . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵) → [𝑎] ∼ ∈
(Base‘𝑄)) | 
| 39 | 5, 37, 38 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → [𝑎] ∼ ∈
(Base‘𝑄)) | 
| 40 | 5, 8, 9, 10, 1, 11, 12 | rngqiprngghmlem1 21298 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( 1 · 𝑎) ∈ (Base‘𝐽)) | 
| 41 | 40 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( 1 · 𝑎) ∈ (Base‘𝐽)) | 
| 42 |  | simpr 484 | . . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) | 
| 43 | 13, 14, 1, 32 | quseccl0 19204 | . . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵) → [𝑏] ∼ ∈
(Base‘𝑄)) | 
| 44 | 5, 42, 43 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → [𝑏] ∼ ∈
(Base‘𝑄)) | 
| 45 | 5, 8, 9, 10, 1, 11, 12 | rngqiprngghmlem1 21298 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ( 1 · 𝑏) ∈ (Base‘𝐽)) | 
| 46 | 45 | adantrl 716 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( 1 · 𝑏) ∈ (Base‘𝐽)) | 
| 47 | 28, 1, 13, 14 | ecqusaddcl 19212 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ([𝑎] ∼
(+g‘𝑄)[𝑏] ∼ ) ∈
(Base‘𝑄)) | 
| 48 | 5, 8, 9, 10, 1, 11, 12 | rngqiprngghmlem2 21299 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( 1 · 𝑎)(+g‘𝐽)( 1 · 𝑏)) ∈ (Base‘𝐽)) | 
| 49 |  | eqid 2736 | . . . . 5
⊢
(+g‘𝑄) = (+g‘𝑄) | 
| 50 |  | eqid 2736 | . . . . 5
⊢
(+g‘𝐽) = (+g‘𝐽) | 
| 51 | 16, 32, 33, 35, 36, 39, 41, 44, 46, 47, 48, 49, 50, 4 | xpsadd 17620 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (〈[𝑎] ∼ , ( 1 · 𝑎)〉(+g‘𝑃)〈[𝑏] ∼ , ( 1 · 𝑏)〉) = 〈([𝑎] ∼
(+g‘𝑄)[𝑏] ∼ ), (( 1 · 𝑎)(+g‘𝐽)( 1 · 𝑏))〉) | 
| 52 | 31, 51 | eqtr4d 2779 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 〈[(𝑎(+g‘𝑅)𝑏)] ∼ , ( 1 · (𝑎(+g‘𝑅)𝑏))〉 = (〈[𝑎] ∼ , ( 1 · 𝑎)〉(+g‘𝑃)〈[𝑏] ∼ , ( 1 · 𝑏)〉)) | 
| 53 | 5 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑅 ∈ Rng) | 
| 54 | 37 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) | 
| 55 | 42 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) | 
| 56 | 1, 3 | rngacl 20160 | . . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 57 | 53, 54, 55, 56 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 58 | 5, 8, 9, 10, 1, 11, 12, 13, 14, 15, 16, 20 | rngqiprngimfv 21309 | . . . 4
⊢ ((𝜑 ∧ (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = 〈[(𝑎(+g‘𝑅)𝑏)] ∼ , ( 1 · (𝑎(+g‘𝑅)𝑏))〉) | 
| 59 | 57, 58 | syldan 591 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = 〈[(𝑎(+g‘𝑅)𝑏)] ∼ , ( 1 · (𝑎(+g‘𝑅)𝑏))〉) | 
| 60 | 5, 8, 9, 10, 1, 11, 12, 13, 14, 15, 16, 20 | rngqiprngimfv 21309 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) | 
| 61 | 60 | adantrr 717 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) | 
| 62 | 5, 8, 9, 10, 1, 11, 12, 13, 14, 15, 16, 20 | rngqiprngimfv 21309 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = 〈[𝑏] ∼ , ( 1 · 𝑏)〉) | 
| 63 | 62 | adantrl 716 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) = 〈[𝑏] ∼ , ( 1 · 𝑏)〉) | 
| 64 | 61, 63 | oveq12d 7450 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(+g‘𝑃)(𝐹‘𝑏)) = (〈[𝑎] ∼ , ( 1 · 𝑎)〉(+g‘𝑃)〈[𝑏] ∼ , ( 1 · 𝑏)〉)) | 
| 65 | 52, 59, 64 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = ((𝐹‘𝑎)(+g‘𝑃)(𝐹‘𝑏))) | 
| 66 | 1, 2, 3, 4, 7, 19,
24, 65 | isghmd 19244 | 1
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑃)) |