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 biimpi ⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
40 39 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
41 10 40 anim12i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
42 41 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
43 simp3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
44 eqid ⊢ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) )
45 eqid ⊢ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
46 8 44 3 6 45 mavmulsolcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
47 46 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 ∈ 𝑉 )
48 37 42 43 47 syl21anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 ∈ 𝑉 )
49 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
50 49 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐼 ∈ 𝑁 )
51 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
52 1 2 3 51 ma1repvcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
53 4 52 eqeltrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → 𝐸 ∈ 𝐵 )
54 33 48 50 53 syl12anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐸 ∈ 𝐵 )
55 20 eqcomd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
56 55 ad2ant2r ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
57 56 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
58 54 57 eleqtrrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐸 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
59 7 8 9 11 15 15 15 29 58 mamuval ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) ) )
60 31 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑅 ∈ Ring )
61 60 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
62 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
63 62 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑋 ∈ 𝐵 )
64 63 48 50 3jca ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
65 64 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
66 simp2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
67 simp3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
68 43 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
69 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
70 1 2 3 51 69 4 6 mulmarep1gsum2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) )
71 61 65 66 67 68 70 syl113anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) )
72 71 mpoeq3dva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
73 simpr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
74 73 3ad2ant2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑌 ∈ 𝑉 )
75 eqid ⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
76 1 2 75 3 marepvval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) → ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
77 63 74 50 76 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
78 5 77 syl5req ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) = 𝐻 )
79 59 72 78 3eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = 𝐻 )