| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) | 
| 2 |  | eqid 2737 | . . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 3 | 1, 2 | mgpbas 20142 | . . 3
⊢
(Base‘𝑌) =
(Base‘(mulGrp‘𝑌)) | 
| 4 |  | eqid 2737 | . . . 4
⊢
(1r‘𝑌) = (1r‘𝑌) | 
| 5 | 1, 4 | ringidval 20180 | . . 3
⊢
(1r‘𝑌) = (0g‘(mulGrp‘𝑌)) | 
| 6 |  | eqid 2737 | . . . 4
⊢
(.r‘𝑌) = (.r‘𝑌) | 
| 7 | 1, 6 | mgpplusg 20141 | . . 3
⊢
(.r‘𝑌) = (+g‘(mulGrp‘𝑌)) | 
| 8 |  | xpsringd.s | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 9 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 10 |  | eqid 2737 | . . . . . . 7
⊢
(1r‘𝑆) = (1r‘𝑆) | 
| 11 | 9, 10 | ringidcl 20262 | . . . . . 6
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) | 
| 12 | 8, 11 | syl 17 | . . . . 5
⊢ (𝜑 → (1r‘𝑆) ∈ (Base‘𝑆)) | 
| 13 |  | xpsringd.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 14 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 15 |  | eqid 2737 | . . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 16 | 14, 15 | ringidcl 20262 | . . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 17 | 13, 16 | syl 17 | . . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 18 | 12, 17 | opelxpd 5724 | . . . 4
⊢ (𝜑 →
〈(1r‘𝑆), (1r‘𝑅)〉 ∈ ((Base‘𝑆) × (Base‘𝑅))) | 
| 19 |  | xpsringd.y | . . . . 5
⊢ 𝑌 = (𝑆 ×s 𝑅) | 
| 20 | 19, 9, 14, 8, 13 | xpsbas 17617 | . . . 4
⊢ (𝜑 → ((Base‘𝑆) × (Base‘𝑅)) = (Base‘𝑌)) | 
| 21 | 18, 20 | eleqtrd 2843 | . . 3
⊢ (𝜑 →
〈(1r‘𝑆), (1r‘𝑅)〉 ∈ (Base‘𝑌)) | 
| 22 | 20 | eleq2d 2827 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑆) × (Base‘𝑅)) ↔ 𝑥 ∈ (Base‘𝑌))) | 
| 23 |  | elxp2 5709 | . . . . . 6
⊢ (𝑥 ∈ ((Base‘𝑆) × (Base‘𝑅)) ↔ ∃𝑎 ∈ (Base‘𝑆)∃𝑏 ∈ (Base‘𝑅)𝑥 = 〈𝑎, 𝑏〉) | 
| 24 | 8 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑆 ∈ Ring) | 
| 25 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑅 ∈ Ring) | 
| 26 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (1r‘𝑆) ∈ (Base‘𝑆)) | 
| 27 | 17 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 28 |  | simprl 771 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑎 ∈ (Base‘𝑆)) | 
| 29 |  | simprr 773 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ (Base‘𝑅)) | 
| 30 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(.r‘𝑆) = (.r‘𝑆) | 
| 31 | 9, 30, 24, 26, 28 | ringcld 20257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → ((1r‘𝑆)(.r‘𝑆)𝑎) ∈ (Base‘𝑆)) | 
| 32 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 33 | 14, 32, 25, 27, 29 | ringcld 20257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → ((1r‘𝑅)(.r‘𝑅)𝑏) ∈ (Base‘𝑅)) | 
| 34 | 19, 9, 14, 24, 25, 26, 27, 28, 29, 31, 33, 30, 32, 6 | xpsmul 17620 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)〈𝑎, 𝑏〉) = 〈((1r‘𝑆)(.r‘𝑆)𝑎), ((1r‘𝑅)(.r‘𝑅)𝑏)〉) | 
| 35 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑎 ∈ (Base‘𝑆)) | 
| 36 | 9, 30, 10 | ringlidm 20266 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑆)) →
((1r‘𝑆)(.r‘𝑆)𝑎) = 𝑎) | 
| 37 | 8, 35, 36 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → ((1r‘𝑆)(.r‘𝑆)𝑎) = 𝑎) | 
| 38 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑏 ∈ (Base‘𝑅)) | 
| 39 | 14, 32, 15 | ringlidm 20266 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑏) = 𝑏) | 
| 40 | 13, 38, 39 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → ((1r‘𝑅)(.r‘𝑅)𝑏) = 𝑏) | 
| 41 | 37, 40 | opeq12d 4881 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → 〈((1r‘𝑆)(.r‘𝑆)𝑎), ((1r‘𝑅)(.r‘𝑅)𝑏)〉 = 〈𝑎, 𝑏〉) | 
| 42 | 34, 41 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)〈𝑎, 𝑏〉) = 〈𝑎, 𝑏〉) | 
| 43 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏〉 →
(〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)〈𝑎, 𝑏〉)) | 
| 44 |  | id 22 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏〉 → 𝑥 = 〈𝑎, 𝑏〉) | 
| 45 | 43, 44 | eqeq12d 2753 | . . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏〉 →
((〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = 𝑥 ↔ (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)〈𝑎, 𝑏〉) = 〈𝑎, 𝑏〉)) | 
| 46 | 42, 45 | syl5ibrcom 247 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑥 = 〈𝑎, 𝑏〉 →
(〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = 𝑥)) | 
| 47 | 46 | rexlimdvva 3213 | . . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ (Base‘𝑆)∃𝑏 ∈ (Base‘𝑅)𝑥 = 〈𝑎, 𝑏〉 →
(〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = 𝑥)) | 
| 48 | 23, 47 | biimtrid 242 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑆) × (Base‘𝑅)) → (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = 𝑥)) | 
| 49 | 22, 48 | sylbird 260 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) → (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = 𝑥)) | 
| 50 | 49 | imp 406 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → (〈(1r‘𝑆), (1r‘𝑅)〉(.r‘𝑌)𝑥) = 𝑥) | 
| 51 | 9, 30, 24, 28, 26 | ringcld 20257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(.r‘𝑆)(1r‘𝑆)) ∈ (Base‘𝑆)) | 
| 52 | 14, 32, 25, 29, 27 | ringcld 20257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑏(.r‘𝑅)(1r‘𝑅)) ∈ (Base‘𝑅)) | 
| 53 | 19, 9, 14, 24, 25, 28, 29, 26, 27, 51, 52, 30, 32, 6 | xpsmul 17620 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (〈𝑎, 𝑏〉(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 〈(𝑎(.r‘𝑆)(1r‘𝑆)), (𝑏(.r‘𝑅)(1r‘𝑅))〉) | 
| 54 | 9, 30, 10 | ringridm 20267 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑆)) → (𝑎(.r‘𝑆)(1r‘𝑆)) = 𝑎) | 
| 55 | 8, 35, 54 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(.r‘𝑆)(1r‘𝑆)) = 𝑎) | 
| 56 | 14, 32, 15 | ringridm 20267 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑅)) → (𝑏(.r‘𝑅)(1r‘𝑅)) = 𝑏) | 
| 57 | 13, 38, 56 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑏(.r‘𝑅)(1r‘𝑅)) = 𝑏) | 
| 58 | 55, 57 | opeq12d 4881 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → 〈(𝑎(.r‘𝑆)(1r‘𝑆)), (𝑏(.r‘𝑅)(1r‘𝑅))〉 = 〈𝑎, 𝑏〉) | 
| 59 | 53, 58 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (〈𝑎, 𝑏〉(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 〈𝑎, 𝑏〉) | 
| 60 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = (〈𝑎, 𝑏〉(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉)) | 
| 61 | 60, 44 | eqeq12d 2753 | . . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 𝑥 ↔ (〈𝑎, 𝑏〉(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 〈𝑎, 𝑏〉)) | 
| 62 | 59, 61 | syl5ibrcom 247 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑥 = 〈𝑎, 𝑏〉 → (𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 𝑥)) | 
| 63 | 62 | rexlimdvva 3213 | . . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ (Base‘𝑆)∃𝑏 ∈ (Base‘𝑅)𝑥 = 〈𝑎, 𝑏〉 → (𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 𝑥)) | 
| 64 | 23, 63 | biimtrid 242 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝑆) × (Base‘𝑅)) → (𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 𝑥)) | 
| 65 | 22, 64 | sylbird 260 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) → (𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 𝑥)) | 
| 66 | 65 | imp 406 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → (𝑥(.r‘𝑌)〈(1r‘𝑆), (1r‘𝑅)〉) = 𝑥) | 
| 67 | 3, 5, 7, 21, 50, 66 | ismgmid2 18681 | . 2
⊢ (𝜑 →
〈(1r‘𝑆), (1r‘𝑅)〉 = (1r‘𝑌)) | 
| 68 | 67 | eqcomd 2743 | 1
⊢ (𝜑 → (1r‘𝑌) =
〈(1r‘𝑆), (1r‘𝑅)〉) |