Metamath Proof Explorer

Theorem 1marepvmarrepid

Description: Replacing the ith row by 0's and the ith component of a (column) vector at the diagonal position for the identity matrix with the ith column replaced by the vector results in the matrix itself. (Contributed by AV, 14-Feb-2019) (Revised by AV, 27-Feb-2019)

Ref Expression
Hypotheses marepvmarrep1.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
marepvmarrep1.o ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
marepvmarrep1.x ⊢ 𝑋 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
Assertion 1marepvmarrepid ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐼 ( 𝑋 ( 𝑁 matRRep 𝑅 ) ( 𝑍 ‘ 𝐼 ) ) 𝐼 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 marepvmarrep1.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
2 marepvmarrep1.o ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
3 marepvmarrep1.x ⊢ 𝑋 = ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
4 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
5 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
6 4 5 1 2 ma1repvcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
7 6 ancom2s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
8 3 7 eqeltrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑋 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
9 elmapi ⊢ ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → 𝑍 : 𝑁 ⟶ ( Base ‘ 𝑅 ) )
10 ffvelrn ⊢ ( ( 𝑍 : 𝑁 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑁 ) → ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
11 10 ex ⊢ ( 𝑍 : 𝑁 ⟶ ( Base ‘ 𝑅 ) → ( 𝐼 ∈ 𝑁 → ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
12 9 11 syl ⊢ ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → ( 𝐼 ∈ 𝑁 → ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
13 12 1 eleq2s ⊢ ( 𝑍 ∈ 𝑉 → ( 𝐼 ∈ 𝑁 → ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
14 13 impcom ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
15 14 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
16 simpl ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) → 𝐼 ∈ 𝑁 )
17 16 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝐼 ∈ 𝑁 )
18 eqid ⊢ ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep 𝑅 )
19 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20 4 5 18 19 marrepval ⊢ ( ( ( 𝑋 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ ( 𝑍 ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ( 𝑁 matRRep 𝑅 ) ( 𝑍 ‘ 𝐼 ) ) 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) ) )
21 8 15 17 17 20 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐼 ( 𝑋 ( 𝑁 matRRep 𝑅 ) ( 𝑍 ‘ 𝐼 ) ) 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) ) )
22 iftrue ⊢ ( 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) )
23 22 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) )
24 iftrue ⊢ ( 𝑗 = 𝐼 → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑍 ‘ 𝐼 ) )
25 24 adantr ⊢ ( ( 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑍 ‘ 𝐼 ) )
26 iftrue ⊢ ( 𝑗 = 𝐼 → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) = ( 𝑍 ‘ 𝑖 ) )
27 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑍 ‘ 𝑖 ) = ( 𝑍 ‘ 𝐼 ) )
28 27 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) = ( 𝑍 ‘ 𝐼 ) )
29 26 28 sylan9eq ⊢ ( ( 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) = ( 𝑍 ‘ 𝐼 ) )
30 25 29 eqtr4d ⊢ ( ( 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
31 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
32 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝑁 ∈ Fin )
33 32 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑁 ∈ Fin )
34 33 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑁 ∈ Fin )
35 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝑅 ∈ Ring )
36 35 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑅 ∈ Ring )
37 36 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
38 simp2 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
39 simp3 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
40 4 31 19 34 37 38 39 2 mat1ov ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 1 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
41 40 adantl ⊢ ( ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 1 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
42 41 adantl ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( 𝑖 1 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
43 eqtr2 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑖 = 𝑗 ) → 𝐼 = 𝑗 )
44 43 eqcomd ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑖 = 𝑗 ) → 𝑗 = 𝐼 )
45 44 ex ⊢ ( 𝑖 = 𝐼 → ( 𝑖 = 𝑗 → 𝑗 = 𝐼 ) )
46 45 con3d ⊢ ( 𝑖 = 𝐼 → ( ¬ 𝑗 = 𝐼 → ¬ 𝑖 = 𝑗 ) )
47 46 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ¬ 𝑗 = 𝐼 → ¬ 𝑖 = 𝑗 ) )
48 47 impcom ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ¬ 𝑖 = 𝑗 )
49 iffalse ⊢ ( ¬ 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
50 48 49 syl ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
51 42 50 eqtrd ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → ( 𝑖 1 𝑗 ) = ( 0g ‘ 𝑅 ) )
52 iffalse ⊢ ( ¬ 𝑗 = 𝐼 → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) = ( 𝑖 1 𝑗 ) )
53 52 adantr ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) = ( 𝑖 1 𝑗 ) )
54 iffalse ⊢ ( ¬ 𝑗 = 𝐼 → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
55 54 adantr ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
56 51 53 55 3eqtr4rd ⊢ ( ( ¬ 𝑗 = 𝐼 ∧ ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
57 30 56 pm2.61ian ⊢ ( ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
58 23 57 eqtrd ⊢ ( ( 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
59 iffalse ⊢ ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = ( 𝑖 𝑋 𝑗 ) )
60 59 adantr ⊢ ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = ( 𝑖 𝑋 𝑗 ) )
61 4 5 2 mat1bas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
62 61 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
63 simpr ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) → 𝑍 ∈ 𝑉 )
64 63 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑍 ∈ 𝑉 )
65 62 64 17 3jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
66 65 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) )
67 3simpc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
68 37 66 67 3jca ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
69 68 adantl ⊢ ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 ∈ Ring ∧ ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
70 4 5 1 2 19 3 ma1repveval ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑋 𝑗 ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
71 69 70 syl ⊢ ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑋 𝑗 ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
72 34 ad2antlr ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → 𝑁 ∈ Fin )
73 37 ad2antlr ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → 𝑅 ∈ Ring )
74 38 ad2antlr ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → 𝑖 ∈ 𝑁 )
75 39 ad2antlr ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → 𝑗 ∈ 𝑁 )
76 4 31 19 72 73 74 75 2 mat1ov ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → ( 𝑖 1 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
77 equcom ⊢ ( 𝑖 = 𝑗 ↔ 𝑗 = 𝑖 )
78 77 a1i ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → ( 𝑖 = 𝑗 ↔ 𝑗 = 𝑖 ) )
79 78 ifbid ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
80 76 79 eqtr2d ⊢ ( ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ¬ 𝑗 = 𝐼 ) → if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑖 1 𝑗 ) )
81 80 ifeq2da ⊢ ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
82 60 71 81 3eqtrd ⊢ ( ( ¬ 𝑖 = 𝐼 ∧ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
83 58 82 pm2.61ian ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) = if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) )
84 83 mpoeq3dva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝐼 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑋 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) ) )
85 eqid ⊢ ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
86 4 5 85 1 marepvval ⊢ ( ( 1 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) ) )
87 65 86 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 1 ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) ) )
88 3 87 syl5req ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑍 ‘ 𝑖 ) , ( 𝑖 1 𝑗 ) ) ) = 𝑋 )
89 21 84 88 3eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐼 ( 𝑋 ( 𝑁 matRRep 𝑅 ) ( 𝑍 ‘ 𝐼 ) ) 𝐼 ) = 𝑋 )