| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cramerimp.m | . . 3
⊢  × =
(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) | 
| 2 |  | eqid 2737 | . . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 3 |  | eqid 2737 | . . 3
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 4 |  | simpl 482 | . . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ CRing) | 
| 5 | 4 | 3ad2ant1 1134 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing) | 
| 6 |  | cramerimp.a | . . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 7 |  | cramerimp.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐴) | 
| 8 | 6, 7 | matrcl 22416 | . . . . . 6
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) | 
| 9 | 8 | simpld 494 | . . . . 5
⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin) | 
| 11 | 10 | 3ad2ant2 1135 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑁 ∈ Fin) | 
| 12 | 9 | anim2i 617 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin)) | 
| 13 | 12 | ancomd 461 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) | 
| 14 | 6, 2 | matbas2 22427 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑m (𝑁
× 𝑁)) =
(Base‘𝐴)) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴)) | 
| 16 | 7, 15 | eqtr4id 2796 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → 𝐵 = ((Base‘𝑅) ↑m (𝑁 × 𝑁))) | 
| 17 | 16 | eleq2d 2827 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) | 
| 18 | 17 | biimpd 229 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) | 
| 19 | 18 | ex 412 | . . . . . . . . 9
⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝐵 → (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))))) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑋 ∈ 𝐵 → (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))))) | 
| 21 | 20 | com12 32 | . . . . . . 7
⊢ (𝑋 ∈ 𝐵 → ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))))) | 
| 22 | 21 | pm2.43a 54 | . . . . . 6
⊢ (𝑋 ∈ 𝐵 → ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) | 
| 24 | 23 | impcom 407 | . . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) | 
| 25 | 24 | 3adant3 1133 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) | 
| 26 |  | crngring 20242 | . . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 27 | 26 | adantr 480 | . . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 28 | 27, 10 | anim12i 613 | . . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin)) | 
| 29 | 28 | 3adant3 1133 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin)) | 
| 30 |  | ne0i 4341 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑁 → 𝑁 ≠ ∅) | 
| 31 | 30 | adantl 481 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑁 ≠ ∅) | 
| 32 | 31 | 3ad2ant1 1134 | . . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑁 ≠ ∅) | 
| 33 | 11, 11, 32 | 3jca 1129 | . . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅)) | 
| 34 |  | cramerimp.v | . . . . . . . . . . 11
⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) | 
| 35 | 34 | eleq2i 2833 | . . . . . . . . . 10
⊢ (𝑌 ∈ 𝑉 ↔ 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) | 
| 36 | 35 | biimpi 216 | . . . . . . . . 9
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) | 
| 37 | 36 | adantl 481 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) | 
| 38 | 4, 37 | anim12i 613 | . . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑅 ∈ CRing ∧ 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁))) | 
| 39 | 38 | 3adant3 1133 | . . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ CRing ∧ 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁))) | 
| 40 |  | simp3 1139 | . . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 · 𝑍) = 𝑌) | 
| 41 |  | eqid 2737 | . . . . . . . 8
⊢
((Base‘𝑅)
↑m (𝑁
× 𝑁)) =
((Base‘𝑅)
↑m (𝑁
× 𝑁)) | 
| 42 |  | cramerimp.x | . . . . . . . 8
⊢  · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) | 
| 43 |  | eqid 2737 | . . . . . . . 8
⊢
((Base‘𝑅)
↑m 𝑁) =
((Base‘𝑅)
↑m 𝑁) | 
| 44 | 2, 41, 34, 42, 43 | mavmulsolcl 22557 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅) ∧ (𝑅 ∈ CRing ∧ 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁))) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) | 
| 45 | 44 | imp 406 | . . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅) ∧ (𝑅 ∈ CRing ∧ 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁))) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) | 
| 46 | 33, 39, 40, 45 | syl21anc 838 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) | 
| 47 |  | simpr 484 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝐼 ∈ 𝑁) | 
| 48 | 47 | 3ad2ant1 1134 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐼 ∈ 𝑁) | 
| 49 |  | cramerimp.e | . . . . . 6
⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) | 
| 50 |  | eqid 2737 | . . . . . . 7
⊢
(1r‘𝐴) = (1r‘𝐴) | 
| 51 | 6, 7, 34, 50 | ma1repvcl 22576 | . . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵) | 
| 52 | 49, 51 | eqeltrid 2845 | . . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → 𝐸 ∈ 𝐵) | 
| 53 | 29, 46, 48, 52 | syl12anc 837 | . . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸 ∈ 𝐵) | 
| 54 | 16 | eqcomd 2743 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = 𝐵) | 
| 55 | 54 | ad2ant2r 747 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = 𝐵) | 
| 56 | 55 | 3adant3 1133 | . . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = 𝐵) | 
| 57 | 53, 56 | eleqtrrd 2844 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) | 
| 58 | 1, 2, 3, 5, 11, 11, 11, 25, 57 | mamuval 22397 | . 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 × 𝐸) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝑗)))))) | 
| 59 | 27 | 3ad2ant1 1134 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ Ring) | 
| 60 | 59 | 3ad2ant1 1134 | . . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 61 |  | simpl 482 | . . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝐵) | 
| 62 | 61 | 3ad2ant2 1135 | . . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋 ∈ 𝐵) | 
| 63 | 62, 46, 48 | 3jca 1129 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) | 
| 64 | 63 | 3ad2ant1 1134 | . . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) | 
| 65 |  | simp2 1138 | . . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 66 |  | simp3 1139 | . . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) | 
| 67 | 40 | 3ad2ant1 1134 | . . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑋 · 𝑍) = 𝑌) | 
| 68 |  | eqid 2737 | . . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 69 | 6, 7, 34, 50, 68, 49, 42 | mulmarep1gsum2 22580 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ (𝑋 · 𝑍) = 𝑌)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝑗)))) = if(𝑗 = 𝐼, (𝑌‘𝑖), (𝑖𝑋𝑗))) | 
| 70 | 60, 64, 65, 66, 67, 69 | syl113anc 1384 | . . 3
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝑗)))) = if(𝑗 = 𝐼, (𝑌‘𝑖), (𝑖𝑋𝑗))) | 
| 71 | 70 | mpoeq3dva 7510 | . 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝑗))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐼, (𝑌‘𝑖), (𝑖𝑋𝑗)))) | 
| 72 |  | cramerimp.h | . . 3
⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) | 
| 73 |  | simpr 484 | . . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ 𝑉) | 
| 74 | 73 | 3ad2ant2 1135 | . . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑌 ∈ 𝑉) | 
| 75 |  | eqid 2737 | . . . . 5
⊢ (𝑁 matRepV 𝑅) = (𝑁 matRepV 𝑅) | 
| 76 | 6, 7, 75, 34 | marepvval 22573 | . . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁) → ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐼, (𝑌‘𝑖), (𝑖𝑋𝑗)))) | 
| 77 | 62, 74, 48, 76 | syl3anc 1373 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐼, (𝑌‘𝑖), (𝑖𝑋𝑗)))) | 
| 78 | 72, 77 | eqtr2id 2790 | . 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐼, (𝑌‘𝑖), (𝑖𝑋𝑗))) = 𝐻) | 
| 79 | 58, 71, 78 | 3eqtrd 2781 | 1
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 × 𝐸) = 𝐻) |