Metamath Proof Explorer

Theorem cramerimplem2

Description: Lemma 2 for cramerimp : The matrix of a system of linear equations multiplied with the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramerimp.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cramerimp.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cramerimp.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
cramerimp.e ⊢ 𝐸 = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
cramerimp.h ⊢ 𝐻 = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 )
cramerimp.x ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
cramerimp.m ⊢ × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
Assertion cramerimplem2 ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = 𝐻 )

Proof

Step Hyp Ref Expression
1 cramerimp.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cramerimp.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cramerimp.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4 cramerimp.e ⊢ 𝐸 = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
5 cramerimp.h ⊢ 𝐻 = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 )
6 cramerimp.x ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
7 cramerimp.m ⊢ × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ CRing )
11 10 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑅 ∈ CRing )
12 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
13 12 simpld ⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
14 13 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑁 ∈ Fin )
15 14 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑁 ∈ Fin )
16 13 anim2i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) )
17 16 ancomd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
18 1 8 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
19 17 18 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
20 2 19 eqtr4id ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
21 20 eleq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
22 21 biimpd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
23 22 ex ⊢ ( 𝑅 ∈ CRing → ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) )
24 23 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) )
25 24 com12 ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) )
26 25 pm2.43a ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
27 26 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
28 27 impcom ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
29 28 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
30 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
31 30 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ Ring )
32 31 14 anim12i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
33 32 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
34 ne0i ⊢ ( 𝐼 ∈ 𝑁 → 𝑁 ≠ ∅ )
35 34 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑁 ≠ ∅ )
36 35 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑁 ≠ ∅ )
37 15 15 36 3jca ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) )
38 3 eleq2i ⊢ ( 𝑌 ∈ 𝑉 ↔ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
39 38 bilani ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
40 10 39 anim12i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
41 40 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
42 simp3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
43 eqid ⊢ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) )
44 eqid ⊢ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
45 8 43 3 6 44 mavmulsolcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
46 45 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 ∈ 𝑉 )
47 37 41 42 46 syl21anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 ∈ 𝑉 )
48 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
49 48 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐼 ∈ 𝑁 )
50 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
51 1 2 3 50 ma1repvcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
52 4 51 eqeltrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → 𝐸 ∈ 𝐵 )
53 33 47 49 52 syl12anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐸 ∈ 𝐵 )
54 20 eqcomd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
55 54 ad2ant2r ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
56 55 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
57 53 56 eleqtrrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐸 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
58 7 8 9 11 15 15 15 29 57 mamuval ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) ) )
59 31 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑅 ∈ Ring )
60 59 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
61 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
62 61 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑋 ∈ 𝐵 )
63 62 47 49 3jca ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
64 63 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
65 simp2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
66 simp3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
67 42 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
68 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
69 1 2 3 50 68 4 6 mulmarep1gsum2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) )
70 60 64 65 66 67 69 syl113anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) )
71 70 mpoeq3dva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
72 simpr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
73 72 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑌 ∈ 𝑉 )
74 eqid ⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
75 1 2 74 3 marepvval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) → ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
76 62 73 49 75 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
77 5 76 eqtr2id ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) = 𝐻 )
78 58 71 77 3eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = 𝐻 )