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	eqtr2id	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌 ‘ 𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) = 𝐻 )
79	59 72 78	3eqtrd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = 𝐻 )