Metamath Proof Explorer

Theorem scmatf1

Description: There is a 1-1 function from a ring to any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 25-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
Assertion scmatf1 ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1→ 𝐶 )

Proof

Step Hyp Ref Expression
1 scmatrhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
4 scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
5 scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
6 scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
7 1 2 3 4 5 6 scmatf ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ 𝐶 )
8 7 3adant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ 𝐶 )
9 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
10 simpl ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → 𝑦 ∈ 𝐾 )
11 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ∗ 1 ) )
12 9 10 11 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ∗ 1 ) )
13 simpr ⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → 𝑧 ∈ 𝐾 )
14 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ∗ 1 ) )
15 9 13 14 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ∗ 1 ) )
16 12 15 eqeq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑦 ∗ 1 ) = ( 𝑧 ∗ 1 ) ) )
17 16 3adantl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑦 ∗ 1 ) = ( 𝑧 ∗ 1 ) ) )
18 2 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
19 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
20 19 3 ringidcl ⊢ ( 𝐴 ∈ Ring → 1 ∈ ( Base ‘ 𝐴 ) )
21 18 20 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝐴 ) )
22 21 10 anim12ci ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑦 ∈ 𝐾 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) )
23 1 2 19 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑦 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
24 22 23 syldan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑦 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
25 21 13 anim12ci ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑧 ∈ 𝐾 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) )
26 1 2 19 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑧 ∈ 𝐾 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑧 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
27 25 26 syldan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑧 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) )
28 24 27 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑧 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ) )
29 28 3adantl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑧 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ) )
30 2 19 eqmat ⊢ ( ( ( 𝑦 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑧 ∗ 1 ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑦 ∗ 1 ) = ( 𝑧 ∗ 1 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ) )
31 29 30 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ∗ 1 ) = ( 𝑧 ∗ 1 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ) )
32 difsnid ⊢ ( 𝑖 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) = 𝑁 )
33 32 eqcomd ⊢ ( 𝑖 ∈ 𝑁 → 𝑁 = ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) )
34 33 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → 𝑁 = ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) )
35 34 raleqdv ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ∀ 𝑗 ∈ ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ) )
36 oveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) )
37 oveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) )
38 36 37 eqeq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) ) )
39 38 ralunsn ⊢ ( 𝑖 ∈ 𝑁 → ( ∀ 𝑗 ∈ ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) ) ) )
40 39 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) ) ) )
41 10 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐾 ) )
42 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐾 ) )
43 41 42 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) )
44 id ⊢ ( 𝑖 ∈ 𝑁 → 𝑖 ∈ 𝑁 )
45 44 44 jca ⊢ ( 𝑖 ∈ 𝑁 → ( 𝑖 ∈ 𝑁 ∧ 𝑖 ∈ 𝑁 ) )
46 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
47 2 1 46 3 4 scmatscmide ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑖 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = if ( 𝑖 = 𝑖 , 𝑦 , ( 0g ‘ 𝑅 ) ) )
48 43 45 47 syl2an ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = if ( 𝑖 = 𝑖 , 𝑦 , ( 0g ‘ 𝑅 ) ) )
49 eqid ⊢ 𝑖 = 𝑖
50 49 iftruei ⊢ if ( 𝑖 = 𝑖 , 𝑦 , ( 0g ‘ 𝑅 ) ) = 𝑦
51 48 50 eqtrdi ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = 𝑦 )
52 13 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑧 ∈ 𝐾 ) )
53 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑧 ∈ 𝐾 ) )
54 52 53 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾 ) )
55 2 1 46 3 4 scmatscmide ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑖 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) = if ( 𝑖 = 𝑖 , 𝑧 , ( 0g ‘ 𝑅 ) ) )
56 54 45 55 syl2an ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) = if ( 𝑖 = 𝑖 , 𝑧 , ( 0g ‘ 𝑅 ) ) )
57 49 iftruei ⊢ if ( 𝑖 = 𝑖 , 𝑧 , ( 0g ‘ 𝑅 ) ) = 𝑧
58 56 57 eqtrdi ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) = 𝑧 )
59 51 58 eqeq12d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) ↔ 𝑦 = 𝑧 ) )
60 59 anbi2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ ( 𝑖 ( 𝑦 ∗ 1 ) 𝑖 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑖 ) ) ↔ ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) ) )
61 35 40 60 3bitrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) ) )
62 61 ralbidva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ∀ 𝑖 ∈ 𝑁 ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) ) )
63 62 3adantl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ↔ ∀ 𝑖 ∈ 𝑁 ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) ) )
64 r19.26 ⊢ ( ∀ 𝑖 ∈ 𝑁 ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) ↔ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ ∀ 𝑖 ∈ 𝑁 𝑦 = 𝑧 ) )
65 rspn0 ⊢ ( 𝑁 ≠ ∅ → ( ∀ 𝑖 ∈ 𝑁 𝑦 = 𝑧 → 𝑦 = 𝑧 ) )
66 65 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( ∀ 𝑖 ∈ 𝑁 𝑦 = 𝑧 → 𝑦 = 𝑧 ) )
67 66 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ 𝑁 𝑦 = 𝑧 → 𝑦 = 𝑧 ) )
68 67 com12 ⊢ ( ∀ 𝑖 ∈ 𝑁 𝑦 = 𝑧 → ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑦 = 𝑧 ) )
69 64 68 simplbiim ⊢ ( ∀ 𝑖 ∈ 𝑁 ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑦 = 𝑧 ) )
70 69 com12 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ 𝑁 ( ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝑖 } ) ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) )
71 63 70 sylbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑦 ∗ 1 ) 𝑗 ) = ( 𝑖 ( 𝑧 ∗ 1 ) 𝑗 ) → 𝑦 = 𝑧 ) )
72 31 71 sylbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ∗ 1 ) = ( 𝑧 ∗ 1 ) → 𝑦 = 𝑧 ) )
73 17 72 sylbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
74 73 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐾 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
75 dff13 ⊢ ( 𝐹 : 𝐾 –1-1→ 𝐶 ↔ ( 𝐹 : 𝐾 ⟶ 𝐶 ∧ ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐾 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
76 8 74 75 sylanbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1→ 𝐶 )