This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem madufval

Description: First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
madufval.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
madufval.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
madufval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madufval.o ⊢ 1 = ( 1r ‘ 𝑅 )
madufval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion madufval 𝐽 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 madufval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 madufval.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
3 madufval.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
4 madufval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
5 madufval.o ⊢ 1 = ( 1r ‘ 𝑅 )
6 madufval.z ⊢ 0 = ( 0g ‘ 𝑅 )
7 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ ( 𝑁 Mat 𝑟 ) ) )
8 id ⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
9 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 maDet 𝑟 ) = ( 𝑁 maDet 𝑟 ) )
10 eqidd ⊢ ( 𝑛 = 𝑁 → if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) = if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) )
11 8 8 10 mpoeq123dv ⊢ ( 𝑛 = 𝑁 → ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) )
12 9 11 fveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) = ( ( 𝑁 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) )
13 8 8 12 mpoeq123dv ⊢ ( 𝑛 = 𝑁 → ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
14 7 13 mpteq12dv ⊢ ( 𝑛 = 𝑁 → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) = ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
15 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑁 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
16 15 fveq2d ⊢ ( 𝑟 = 𝑅 → ( Base ‘ ( 𝑁 Mat 𝑟 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
17 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑁 maDet 𝑟 ) = ( 𝑁 maDet 𝑅 ) )
18 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
19 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
20 18 19 ifeq12d ⊢ ( 𝑟 = 𝑅 → if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) = if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
21 20 ifeq1d ⊢ ( 𝑟 = 𝑅 → if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) = if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) )
22 21 mpoeq3dv ⊢ ( 𝑟 = 𝑅 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) )
23 17 22 fveq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑁 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) )
24 23 mpoeq3dv ⊢ ( 𝑟 = 𝑅 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
25 16 24 mpteq12dv ⊢ ( 𝑟 = 𝑅 → ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) = ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
26 df-madu ⊢ maAdju = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
27 fvex ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∈ V
28 27 mptex ⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) ∈ V
29 14 25 26 28 ovmpo ⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maAdju 𝑅 ) = ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
30 1 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
31 4 30 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
32 5 a1i ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 1 = ( 1r ‘ 𝑅 ) )
33 6 a1i ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 0 = ( 0g ‘ 𝑅 ) )
34 32 33 ifeq12d ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → if ( 𝑙 = 𝑖 , 1 , 0 ) = if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
35 34 ifeq1d ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) = if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) )
36 35 mpoeq3ia ⊢ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) )
37 2 36 fveq12i ⊢ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) )
38 37 a1i ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) )
39 38 mpoeq3ia ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) )
40 31 39 mpteq12i ⊢ ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) = ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
41 29 40 eqtr4di ⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maAdju 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
42 26 reldmmpo ⊢ Rel dom maAdju
43 42 ovprc ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maAdju 𝑅 ) = ∅ )
44 df-mat ⊢ Mat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ ) )
45 44 reldmmpo ⊢ Rel dom Mat
46 45 ovprc ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ∅ )
47 1 46 eqtrid ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝐴 = ∅ )
48 47 fveq2d ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ 𝐴 ) = ( Base ‘ ∅ ) )
49 base0 ⊢ ∅ = ( Base ‘ ∅ )
50 48 4 49 3eqtr4g ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
51 50 mpteq1d ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) = ( 𝑚 ∈ ∅ ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
52 mpt0 ⊢ ( 𝑚 ∈ ∅ ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) = ∅
53 51 52 eqtrdi ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) = ∅ )
54 43 53 eqtr4d ⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 maAdju 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
55 41 54 pm2.61i ⊢ ( 𝑁 maAdju 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
56 3 55 eqtri ⊢ 𝐽 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )