Metamath Proof Explorer

Theorem madutpos

Description: The adjuct of a transposed matrix is the transposition of the adjunct of the matrix. (Contributed by Stefan O'Rear, 17-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 maduf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 maduf.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
3 maduf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 eqid ⊢ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) )
5 4 tposmpo ⊢ tpos ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) = ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) )
6 orcom ⊢ ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) ↔ ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) )
7 6 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) ↔ ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) ) )
8 ancom ⊢ ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) ↔ ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) )
9 8 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) ↔ ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) ) )
10 9 ifbid ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
11 ovtpos ⊢ ( 𝑐 tpos 𝑀 𝑑 ) = ( 𝑑 𝑀 𝑐 )
12 11 eqcomi ⊢ ( 𝑑 𝑀 𝑐 ) = ( 𝑐 tpos 𝑀 𝑑 )
13 12 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑑 𝑀 𝑐 ) = ( 𝑐 tpos 𝑀 𝑑 ) )
14 7 10 13 ifbieq12d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) = if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) )
15 14 mpoeq3dv ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) = ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) ) )
16 5 15 eqtrid ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → tpos ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) = ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) ) )
17 16 fveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ tpos ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) ) ) )
18 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑅 ∈ CRing )
19 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20 1 3 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
21 20 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
22 21 ad2antlr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
23 simp1ll ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → 𝑅 ∈ CRing )
24 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
25 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26 19 25 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
28 19 27 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29 26 28 ifcld ⊢ ( 𝑅 ∈ Ring → if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
30 23 24 29 3syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
31 1 19 3 matbas2i ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
32 elmapi ⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
33 31 32 syl ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
34 33 ad2antlr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
35 34 fovrnda ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ ( 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) ) → ( 𝑑 𝑀 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
36 35 3impb ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → ( 𝑑 𝑀 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
37 30 36 ifcld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ∈ ( Base ‘ 𝑅 ) )
38 1 19 3 22 18 37 matbas2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ∈ 𝐵 )
39 eqid ⊢ ( 𝑁 maDet 𝑅 ) = ( 𝑁 maDet 𝑅 )
40 39 1 3 mdettpos ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑅 ) ‘ tpos ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
41 18 38 40 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ tpos ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
42 17 41 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
43 1 3 mattposcl ⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )
44 43 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → tpos 𝑀 ∈ 𝐵 )
45 44 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → tpos 𝑀 ∈ 𝐵 )
46 simprl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
47 simprr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
48 1 39 2 3 25 27 maducoeval2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ tpos 𝑀 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) ) ) )
49 18 45 46 47 48 syl211anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑐 ∈ 𝑁 , 𝑑 ∈ 𝑁 ↦ if ( ( 𝑐 = 𝑏 ∨ 𝑑 = 𝑎 ) , if ( ( 𝑑 = 𝑎 ∧ 𝑐 = 𝑏 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑐 tpos 𝑀 𝑑 ) ) ) ) )
50 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑀 ∈ 𝐵 )
51 1 39 2 3 25 27 maducoeval2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝑁 ∧ 𝑎 ∈ 𝑁 ) → ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝑎 ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
52 18 50 47 46 51 syl211anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝑎 ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( ( 𝑑 = 𝑎 ∨ 𝑐 = 𝑏 ) , if ( ( 𝑐 = 𝑏 ∧ 𝑑 = 𝑎 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
53 42 49 52 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝑎 ) )
54 ovtpos ⊢ ( 𝑎 tpos ( 𝐽 ‘ 𝑀 ) 𝑏 ) = ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝑎 )
55 53 54 eqtr4di ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( 𝑎 tpos ( 𝐽 ‘ 𝑀 ) 𝑏 ) )
56 55 ralrimivva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( 𝑎 tpos ( 𝐽 ‘ 𝑀 ) 𝑏 ) )
57 1 2 3 maduf ⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )
58 57 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐽 : 𝐵 ⟶ 𝐵 )
59 58 44 ffvelrnd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ tpos 𝑀 ) ∈ 𝐵 )
60 1 19 3 matbas2i ⊢ ( ( 𝐽 ‘ tpos 𝑀 ) ∈ 𝐵 → ( 𝐽 ‘ tpos 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
61 59 60 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ tpos 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
62 elmapi ⊢ ( ( 𝐽 ‘ tpos 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → ( 𝐽 ‘ tpos 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
63 ffn ⊢ ( ( 𝐽 ‘ tpos 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → ( 𝐽 ‘ tpos 𝑀 ) Fn ( 𝑁 × 𝑁 ) )
64 61 62 63 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ tpos 𝑀 ) Fn ( 𝑁 × 𝑁 ) )
65 57 ffvelrnda ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
66 1 3 mattposcl ⊢ ( ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 → tpos ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
67 1 19 3 matbas2i ⊢ ( tpos ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 → tpos ( 𝐽 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
68 65 66 67 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → tpos ( 𝐽 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
69 elmapi ⊢ ( tpos ( 𝐽 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → tpos ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
70 ffn ⊢ ( tpos ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → tpos ( 𝐽 ‘ 𝑀 ) Fn ( 𝑁 × 𝑁 ) )
71 68 69 70 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → tpos ( 𝐽 ‘ 𝑀 ) Fn ( 𝑁 × 𝑁 ) )
72 eqfnov2 ⊢ ( ( ( 𝐽 ‘ tpos 𝑀 ) Fn ( 𝑁 × 𝑁 ) ∧ tpos ( 𝐽 ‘ 𝑀 ) Fn ( 𝑁 × 𝑁 ) ) → ( ( 𝐽 ‘ tpos 𝑀 ) = tpos ( 𝐽 ‘ 𝑀 ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( 𝑎 tpos ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) )
73 64 71 72 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐽 ‘ tpos 𝑀 ) = tpos ( 𝐽 ‘ 𝑀 ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝐽 ‘ tpos 𝑀 ) 𝑏 ) = ( 𝑎 tpos ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) )
74 56 73 mpbird ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ tpos 𝑀 ) = tpos ( 𝐽 ‘ 𝑀 ) )