Metamath Proof Explorer

Theorem mdetunilem7

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetuni.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetuni.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetuni.0g ⊢ 0 = ( 0g ‘ 𝑅 )
mdetuni.1r ⊢ 1 = ( 1r ‘ 𝑅 )
mdetuni.pg ⊢ + = ( +g ‘ 𝑅 )
mdetuni.tg ⊢ · = ( .r ‘ 𝑅 )
mdetuni.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mdetuni.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mdetuni.ff ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
mdetuni.al ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
mdetuni.li ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
mdetuni.sc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
Assertion mdetunilem7 ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mdetuni.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mdetuni.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 mdetuni.0g ⊢ 0 = ( 0g ‘ 𝑅 )
5 mdetuni.1r ⊢ 1 = ( 1r ‘ 𝑅 )
6 mdetuni.pg ⊢ + = ( +g ‘ 𝑅 )
7 mdetuni.tg ⊢ · = ( .r ‘ 𝑅 )
8 mdetuni.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
9 mdetuni.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 mdetuni.ff ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
11 mdetuni.al ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
12 mdetuni.li ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
13 mdetuni.sc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
14 fveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑎 ) )
15 14 oveq1d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
16 15 mpoeq3dv ⊢ ( 𝑐 = 𝑑 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
17 16 fveq2d ⊢ ( 𝑐 = 𝑑 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
18 fveq2 ⊢ ( 𝑐 = 𝑑 → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) )
19 18 oveq1d ⊢ ( 𝑐 = 𝑑 → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) )
20 17 19 eqeq12d ⊢ ( 𝑐 = 𝑑 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
21 fveq1 ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( 𝑐 ‘ 𝑎 ) = ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) )
22 21 oveq1d ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) )
23 22 mpoeq3dv ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) )
24 23 fveq2d ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
25 fveq2 ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) )
26 25 oveq1d ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
27 24 26 eqeq12d ⊢ ( 𝑐 = ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) ) )
28 fveq1 ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( 𝑐 ‘ 𝑎 ) = ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) )
29 28 oveq1d ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) )
30 29 mpoeq3dv ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) )
31 30 fveq2d ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
32 fveq2 ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) )
33 32 oveq1d ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) · ( 𝐷 ‘ 𝐹 ) ) )
34 31 33 eqeq12d ⊢ ( 𝑐 = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) · ( 𝐷 ‘ 𝐹 ) ) ) )
35 fveq1 ⊢ ( 𝑐 = 𝐸 → ( 𝑐 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑎 ) )
36 35 oveq1d ⊢ ( 𝑐 = 𝐸 → ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) )
37 36 mpoeq3dv ⊢ ( 𝑐 = 𝐸 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
38 37 fveq2d ⊢ ( 𝑐 = 𝐸 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
39 fveq2 ⊢ ( 𝑐 = 𝐸 → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) )
40 39 oveq1d ⊢ ( 𝑐 = 𝐸 → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ 𝐹 ) ) )
41 38 40 eqeq12d ⊢ ( 𝑐 = 𝐸 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑐 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑐 ) · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
42 eqid ⊢ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) )
43 eqid ⊢ ( +g ‘ ( SymGrp ‘ 𝑁 ) ) = ( +g ‘ ( SymGrp ‘ 𝑁 ) )
44 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
45 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝑁 ∈ Fin )
46 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
47 46 symggrp ⊢ ( 𝑁 ∈ Fin → ( SymGrp ‘ 𝑁 ) ∈ Grp )
48 grpmnd ⊢ ( ( SymGrp ‘ 𝑁 ) ∈ Grp → ( SymGrp ‘ 𝑁 ) ∈ Mnd )
49 45 47 48 3syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( SymGrp ‘ 𝑁 ) ∈ Mnd )
50 eqid ⊢ ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
51 50 46 44 symgtrf ⊢ ran ( pmTrsp ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
52 51 a1i ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ran ( pmTrsp ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
53 eqid ⊢ ( mrCls ‘ ( SubMnd ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( mrCls ‘ ( SubMnd ‘ ( SymGrp ‘ 𝑁 ) ) )
54 50 46 44 53 symggen2 ⊢ ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ ( SymGrp ‘ 𝑁 ) ) ) ‘ ran ( pmTrsp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
55 8 54 syl ⊢ ( 𝜑 → ( ( mrCls ‘ ( SubMnd ‘ ( SymGrp ‘ 𝑁 ) ) ) ‘ ran ( pmTrsp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
56 55 eqcomd ⊢ ( 𝜑 → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( ( mrCls ‘ ( SubMnd ‘ ( SymGrp ‘ 𝑁 ) ) ) ‘ ran ( pmTrsp ‘ 𝑁 ) ) )
57 56 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( ( mrCls ‘ ( SubMnd ‘ ( SymGrp ‘ 𝑁 ) ) ) ‘ ran ( pmTrsp ‘ 𝑁 ) ) )
58 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝑅 ∈ Ring )
59 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐷 : 𝐵 ⟶ 𝐾 )
60 simp3 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
61 59 60 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ 𝐾 )
62 3 7 5 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ 𝐹 ) ∈ 𝐾 ) → ( 1 · ( 𝐷 ‘ 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )
63 58 61 62 syl2anc ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 1 · ( 𝐷 ‘ 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )
64 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
65 9 8 64 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
66 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
67 66 5 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
68 42 67 mhm0 ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = 1 )
69 65 68 syl ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = 1 )
70 69 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = 1 )
71 70 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( 1 · ( 𝐷 ‘ 𝐹 ) ) )
72 46 symgid ⊢ ( 𝑁 ∈ Fin → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
73 8 72 syl ⊢ ( 𝜑 → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
74 73 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
75 74 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
76 75 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( I ↾ 𝑁 ) ‘ 𝑎 ) = ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) )
77 simp2 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
78 fvresi ⊢ ( 𝑎 ∈ 𝑁 → ( ( I ↾ 𝑁 ) ‘ 𝑎 ) = 𝑎 )
79 77 78 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( I ↾ 𝑁 ) ‘ 𝑎 ) = 𝑎 )
80 76 79 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) = 𝑎 )
81 80 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) = ( 𝑎 𝐹 𝑏 ) )
82 81 mpoeq3dva ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 𝑎 𝐹 𝑏 ) ) )
83 1 3 2 matbas2i ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
84 83 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
85 elmapi ⊢ ( 𝐹 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
86 ffn ⊢ ( 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 → 𝐹 Fn ( 𝑁 × 𝑁 ) )
87 84 85 86 3syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 Fn ( 𝑁 × 𝑁 ) )
88 fnov ⊢ ( 𝐹 Fn ( 𝑁 × 𝑁 ) ↔ 𝐹 = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 𝑎 𝐹 𝑏 ) ) )
89 87 88 sylib ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 𝑎 𝐹 𝑏 ) ) )
90 82 89 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) = 𝐹 )
91 90 fveq2d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ 𝐹 ) )
92 63 71 91 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) · ( 𝐷 ‘ 𝐹 ) ) )
93 simp2 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
94 51 sseli ⊢ ( 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) → 𝑒 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
95 94 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
96 46 44 43 symgov ⊢ ( ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) = ( 𝑑 ∘ 𝑒 ) )
97 93 95 96 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) = ( 𝑑 ∘ 𝑒 ) )
98 97 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) = ( ( 𝑑 ∘ 𝑒 ) ‘ 𝑎 ) )
99 98 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) = ( ( 𝑑 ∘ 𝑒 ) ‘ 𝑎 ) )
100 46 44 symgbasf1o ⊢ ( 𝑒 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → 𝑒 : 𝑁 –1-1-onto→ 𝑁 )
101 f1of ⊢ ( 𝑒 : 𝑁 –1-1-onto→ 𝑁 → 𝑒 : 𝑁 ⟶ 𝑁 )
102 95 100 101 3syl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 : 𝑁 ⟶ 𝑁 )
103 102 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑒 : 𝑁 ⟶ 𝑁 )
104 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
105 fvco3 ⊢ ( ( 𝑒 : 𝑁 ⟶ 𝑁 ∧ 𝑎 ∈ 𝑁 ) → ( ( 𝑑 ∘ 𝑒 ) ‘ 𝑎 ) = ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) )
106 103 104 105 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ∘ 𝑒 ) ‘ 𝑎 ) = ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) )
107 99 106 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) = ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) )
108 107 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) )
109 108 mpoeq3dva ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) )
110 109 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) )
111 46 44 symgbasf ⊢ ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → 𝑑 : 𝑁 ⟶ 𝑁 )
112 eqid ⊢ ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
113 112 50 pmtrrn2 ⊢ ( 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) → ∃ 𝑐 ∈ 𝑁 ∃ 𝑓 ∈ 𝑁 ( 𝑐 ≠ 𝑓 ∧ 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ) )
114 simpll1 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝜑 )
115 df-3an ⊢ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓 ) ↔ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) )
116 115 bilanri ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓 ) )
117 84 85 syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
118 117 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
119 118 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
120 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑑 : 𝑁 ⟶ 𝑁 )
121 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑓 ∈ 𝑁 )
122 121 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑓 ∈ 𝑁 )
123 120 122 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( 𝑑 ‘ 𝑓 ) ∈ 𝑁 )
124 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
125 119 123 124 fovcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) ∈ 𝐾 )
126 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑐 ∈ 𝑁 )
127 126 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
128 120 127 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( 𝑑 ‘ 𝑐 ) ∈ 𝑁 )
129 119 128 124 fovcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) ∈ 𝐾 )
130 125 129 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) ∈ 𝐾 ∧ ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) ∈ 𝐾 ) )
131 117 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
132 131 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
133 simp1lr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑑 : 𝑁 ⟶ 𝑁 )
134 simp2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
135 133 134 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑑 ‘ 𝑎 ) ∈ 𝑁 )
136 simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
137 132 135 136 fovcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ∈ 𝐾 )
138 1 2 3 4 5 6 7 8 9 10 11 12 13 114 116 130 137 mdetunilem6 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) ) )
139 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → 𝜑 )
140 fveq2 ⊢ ( 𝑎 = 𝑐 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) )
141 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑁 ∈ Fin )
142 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑐 ∈ 𝑁 )
143 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑓 ∈ 𝑁 )
144 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑐 ≠ 𝑓 )
145 112 pmtrprfv ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) = 𝑓 )
146 141 142 143 144 145 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) = 𝑓 )
147 146 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) = 𝑓 )
148 140 147 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑓 )
149 148 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) = ( 𝑑 ‘ 𝑓 ) )
150 149 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
151 iftrue ⊢ ( 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
152 151 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
153 150 152 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
154 fveq2 ⊢ ( 𝑎 = 𝑓 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑓 ) )
155 prcom ⊢ { 𝑐 , 𝑓 } = { 𝑓 , 𝑐 }
156 155 fveq2i ⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } )
157 156 fveq1i ⊢ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑓 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } ) ‘ 𝑓 )
158 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ Fin )
159 simplrl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) )
160 159 simprd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑓 ∈ 𝑁 )
161 159 simpld ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
162 simplrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑐 ≠ 𝑓 )
163 162 necomd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑓 ≠ 𝑐 )
164 112 pmtrprfv ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝑓 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ∧ 𝑓 ≠ 𝑐 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } ) ‘ 𝑓 ) = 𝑐 )
165 158 160 161 163 164 syl13anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } ) ‘ 𝑓 ) = 𝑐 )
166 157 165 eqtrid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑓 ) = 𝑐 )
167 154 166 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑐 )
168 167 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) = ( 𝑑 ‘ 𝑐 ) )
169 168 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
170 iftrue ⊢ ( 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
171 170 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
172 169 171 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
173 172 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
174 vex ⊢ 𝑎 ∈ V
175 174 elpr ⊢ ( 𝑎 ∈ { 𝑐 , 𝑓 } ↔ ( 𝑎 = 𝑐 ∨ 𝑎 = 𝑓 ) )
176 175 notbii ⊢ ( ¬ 𝑎 ∈ { 𝑐 , 𝑓 } ↔ ¬ ( 𝑎 = 𝑐 ∨ 𝑎 = 𝑓 ) )
177 ioran ⊢ ( ¬ ( 𝑎 = 𝑐 ∨ 𝑎 = 𝑓 ) ↔ ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓 ) )
178 176 177 sylbbr ⊢ ( ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓 ) → ¬ 𝑎 ∈ { 𝑐 , 𝑓 } )
179 178 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ¬ 𝑎 ∈ { 𝑐 , 𝑓 } )
180 prssi ⊢ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) → { 𝑐 , 𝑓 } ⊆ 𝑁 )
181 159 180 syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → { 𝑐 , 𝑓 } ⊆ 𝑁 )
182 pr2ne ⊢ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) → ( { 𝑐 , 𝑓 } ≈ 2o ↔ 𝑐 ≠ 𝑓 ) )
183 159 182 syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑐 , 𝑓 } ≈ 2o ↔ 𝑐 ≠ 𝑓 ) )
184 162 183 mpbird ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → { 𝑐 , 𝑓 } ≈ 2o )
185 112 pmtrmvd ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝑐 , 𝑓 } ⊆ 𝑁 ∧ { 𝑐 , 𝑓 } ≈ 2o ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) = { 𝑐 , 𝑓 } )
186 158 181 184 185 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) = { 𝑐 , 𝑓 } )
187 186 eleq2d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ 𝑎 ∈ { 𝑐 , 𝑓 } ) )
188 187 notbid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ ¬ 𝑎 ∈ { 𝑐 , 𝑓 } ) )
189 188 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ ¬ 𝑎 ∈ { 𝑐 , 𝑓 } ) )
190 179 189 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) )
191 112 pmtrf ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝑐 , 𝑓 } ⊆ 𝑁 ∧ { 𝑐 , 𝑓 } ≈ 2o ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) : 𝑁 ⟶ 𝑁 )
192 158 181 184 191 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) : 𝑁 ⟶ 𝑁 )
193 192 ffnd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) Fn 𝑁 )
194 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
195 fnelnfp ⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) Fn 𝑁 ∧ 𝑎 ∈ 𝑁 ) → ( 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ≠ 𝑎 ) )
196 195 necon2bbid ⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) Fn 𝑁 ∧ 𝑎 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 ↔ ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ) )
197 193 194 196 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 ↔ ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ) )
198 197 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 ↔ ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ) )
199 190 198 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 )
200 199 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) = ( 𝑑 ‘ 𝑎 ) )
201 200 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
202 iffalse ⊢ ( ¬ 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
203 202 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
204 201 203 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
205 173 204 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
206 iffalse ⊢ ( ¬ 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
207 206 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
208 205 207 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
209 153 208 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
210 209 3adant3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
211 210 mpoeq3dva ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
212 139 211 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
213 212 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
214 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝑑 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑐 ) )
215 214 oveq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
216 iftrue ⊢ ( 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
217 215 216 eqtr4d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
218 fveq2 ⊢ ( 𝑎 = 𝑓 → ( 𝑑 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑓 ) )
219 218 oveq1d ⊢ ( 𝑎 = 𝑓 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
220 iftrue ⊢ ( 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
221 219 220 eqtr4d ⊢ ( 𝑎 = 𝑓 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
222 221 adantl ⊢ ( ( ¬ 𝑎 = 𝑐 ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
223 iffalse ⊢ ( ¬ 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
224 223 eqcomd ⊢ ( ¬ 𝑎 = 𝑓 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
225 224 adantl ⊢ ( ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
226 222 225 pm2.61dan ⊢ ( ¬ 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
227 iffalse ⊢ ( ¬ 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
228 226 227 eqtr4d ⊢ ( ¬ 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
229 217 228 pm2.61i ⊢ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
230 229 a1i ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
231 230 mpoeq3ia ⊢ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
232 231 fveq2i ⊢ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
233 232 fveq2i ⊢ ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
234 233 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) ) )
235 138 213 234 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
236 fveq1 ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝑒 ‘ 𝑎 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) )
237 236 fveq2d ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) = ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) )
238 237 oveq1d ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) )
239 238 mpoeq3dv ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) )
240 239 fveqeq2d ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ↔ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
241 235 240 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
242 241 expr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ) → ( 𝑐 ≠ 𝑓 → ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) ) )
243 242 impd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ) → ( ( 𝑐 ≠ 𝑓 ∧ 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
244 243 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → ( ∃ 𝑐 ∈ 𝑁 ∃ 𝑓 ∈ 𝑁 ( 𝑐 ≠ 𝑓 ∧ 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
245 113 244 syl5 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → ( 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
246 245 3impia ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
247 111 246 syl3an2 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
248 110 247 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
249 248 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
250 fveq2 ⊢ ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
251 250 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
252 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
253 58 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑅 ∈ Ring )
254 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
255 254 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
256 66 3 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
257 44 256 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
258 255 257 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
259 258 93 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ∈ 𝐾 )
260 59 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝐷 : 𝐵 ⟶ 𝐾 )
261 simp13 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝐹 ∈ 𝐵 )
262 260 261 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ 𝐾 )
263 3 7 252 253 259 262 ringmneg1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
264 66 7 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
265 44 43 264 mhmlin ⊢ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) ) )
266 255 93 95 265 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) ) )
267 45 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑁 ∈ Fin )
268 simp3 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) )
269 46 44 50 pmtrodpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
270 267 268 269 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
271 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
272 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
273 271 272 5 44 252 zrhpsgnodpm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) = ( ( invg ‘ 𝑅 ) ‘ 1 ) )
274 253 267 270 273 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) = ( ( invg ‘ 𝑅 ) ‘ 1 ) )
275 274 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( invg ‘ 𝑅 ) ‘ 1 ) ) )
276 3 7 5 252 253 259 ringnegr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( invg ‘ 𝑅 ) ‘ 1 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) )
277 266 275 276 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) )
278 277 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
279 263 278 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
280 279 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
281 249 251 280 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
282 simp2 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
283 46 44 elsymgbas ⊢ ( 𝑁 ∈ Fin → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
284 45 283 syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
285 282 284 mpbird ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
286 20 27 34 41 42 43 44 49 52 57 92 281 285 mndind ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ 𝐹 ) ) )