Metamath Proof Explorer

Theorem maduf

Description: Creating the adjunct of matrices is a function from the set of matrices into the set of matrices. (Contributed by Stefan O'Rear, 11-Jul-2018)

Ref Expression
Hypotheses maduf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
maduf.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
maduf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion maduf ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 maduf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 maduf.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
3 maduf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 1 3 matrcl ⊢ ( 𝑚 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6 5 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
7 6 simpld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → 𝑁 ∈ Fin )
8 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → 𝑅 ∈ CRing )
9 eqid ⊢ ( 𝑁 maDet 𝑅 ) = ( 𝑁 maDet 𝑅 )
10 9 1 3 4 mdetf ⊢ ( 𝑅 ∈ CRing → ( 𝑁 maDet 𝑅 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
11 10 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( 𝑁 maDet 𝑅 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
12 11 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑁 maDet 𝑅 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
13 7 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑁 ∈ Fin )
14 simp1l ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ CRing )
15 simp11l ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑅 ∈ CRing )
16 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
17 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
18 4 17 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
19 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20 4 19 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21 18 20 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
22 15 16 21 3syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
23 simp2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
24 simp3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
25 simp11r ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑚 ∈ 𝐵 )
26 1 4 3 23 24 25 matecld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑘 𝑚 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
27 22 26 ifcld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
28 1 4 3 13 14 27 matbas2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ∈ 𝐵 )
29 12 28 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
30 1 4 3 7 8 29 matbas2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ∈ 𝐵 )
31 1 9 2 3 17 19 madufval ⊢ 𝐽 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
32 30 31 fmptd ⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )