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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –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 biimpri ⊢ ( ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) → ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓 ) )
117 116 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓 ) )
118 84 85 syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
119 118 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
120 119 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
121 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑑 : 𝑁 ⟶ 𝑁 )
122 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑓 ∈ 𝑁 )
123 122 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑓 ∈ 𝑁 )
124 121 123 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( 𝑑 ‘ 𝑓 ) ∈ 𝑁 )
125 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
126 120 124 125 fovrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) ∈ 𝐾 )
127 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑐 ∈ 𝑁 )
128 127 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
129 121 128 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( 𝑑 ‘ 𝑐 ) ∈ 𝑁 )
130 120 129 125 fovrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) ∈ 𝐾 )
131 126 130 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) ∈ 𝐾 ∧ ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) ∈ 𝐾 ) )
132 118 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
133 132 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
134 simp1lr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑑 : 𝑁 ⟶ 𝑁 )
135 simp2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
136 134 135 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑑 ‘ 𝑎 ) ∈ 𝑁 )
137 simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
138 133 136 137 fovrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ∈ 𝐾 )
139 1 2 3 4 5 6 7 8 9 10 11 12 13 114 117 131 138 mdetunilem6 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) ) )
140 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → 𝜑 )
141 fveq2 ⊢ ( 𝑎 = 𝑐 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) )
142 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑁 ∈ Fin )
143 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑐 ∈ 𝑁 )
144 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑓 ∈ 𝑁 )
145 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → 𝑐 ≠ 𝑓 )
146 112 pmtrprfv ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) = 𝑓 )
147 142 143 144 145 146 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) = 𝑓 )
148 147 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑐 ) = 𝑓 )
149 141 148 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑓 )
150 149 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) = ( 𝑑 ‘ 𝑓 ) )
151 150 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
152 iftrue ⊢ ( 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
153 152 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
154 151 153 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
155 fveq2 ⊢ ( 𝑎 = 𝑓 → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑓 ) )
156 prcom ⊢ { 𝑐 , 𝑓 } = { 𝑓 , 𝑐 }
157 156 fveq2i ⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } )
158 157 fveq1i ⊢ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑓 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } ) ‘ 𝑓 )
159 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ Fin )
160 simplrl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) )
161 160 simprd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑓 ∈ 𝑁 )
162 160 simpld ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
163 simplrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑐 ≠ 𝑓 )
164 163 necomd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑓 ≠ 𝑐 )
165 112 pmtrprfv ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝑓 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ∧ 𝑓 ≠ 𝑐 ) ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } ) ‘ 𝑓 ) = 𝑐 )
166 159 161 162 164 165 syl13anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑓 , 𝑐 } ) ‘ 𝑓 ) = 𝑐 )
167 158 166 syl5eq ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑓 ) = 𝑐 )
168 155 167 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑐 )
169 168 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) = ( 𝑑 ‘ 𝑐 ) )
170 169 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
171 iftrue ⊢ ( 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
172 171 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
173 170 172 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
174 173 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
175 vex ⊢ 𝑎 ∈ V
176 175 elpr ⊢ ( 𝑎 ∈ { 𝑐 , 𝑓 } ↔ ( 𝑎 = 𝑐 ∨ 𝑎 = 𝑓 ) )
177 176 notbii ⊢ ( ¬ 𝑎 ∈ { 𝑐 , 𝑓 } ↔ ¬ ( 𝑎 = 𝑐 ∨ 𝑎 = 𝑓 ) )
178 ioran ⊢ ( ¬ ( 𝑎 = 𝑐 ∨ 𝑎 = 𝑓 ) ↔ ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓 ) )
179 177 178 sylbbr ⊢ ( ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓 ) → ¬ 𝑎 ∈ { 𝑐 , 𝑓 } )
180 179 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ¬ 𝑎 ∈ { 𝑐 , 𝑓 } )
181 prssi ⊢ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) → { 𝑐 , 𝑓 } ⊆ 𝑁 )
182 160 181 syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → { 𝑐 , 𝑓 } ⊆ 𝑁 )
183 pr2ne ⊢ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) → ( { 𝑐 , 𝑓 } ≈ 2o ↔ 𝑐 ≠ 𝑓 ) )
184 160 183 syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑐 , 𝑓 } ≈ 2o ↔ 𝑐 ≠ 𝑓 ) )
185 163 184 mpbird ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → { 𝑐 , 𝑓 } ≈ 2o )
186 112 pmtrmvd ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝑐 , 𝑓 } ⊆ 𝑁 ∧ { 𝑐 , 𝑓 } ≈ 2o ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) = { 𝑐 , 𝑓 } )
187 159 182 185 186 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) = { 𝑐 , 𝑓 } )
188 187 eleq2d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ 𝑎 ∈ { 𝑐 , 𝑓 } ) )
189 188 notbid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ ¬ 𝑎 ∈ { 𝑐 , 𝑓 } ) )
190 189 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ ¬ 𝑎 ∈ { 𝑐 , 𝑓 } ) )
191 180 190 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) )
192 112 pmtrf ⊢ ( ( 𝑁 ∈ Fin ∧ { 𝑐 , 𝑓 } ⊆ 𝑁 ∧ { 𝑐 , 𝑓 } ≈ 2o ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) : 𝑁 ⟶ 𝑁 )
193 159 182 185 192 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) : 𝑁 ⟶ 𝑁 )
194 193 ffnd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) Fn 𝑁 )
195 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
196 fnelnfp ⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) Fn 𝑁 ∧ 𝑎 ∈ 𝑁 ) → ( 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ↔ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ≠ 𝑎 ) )
197 196 necon2bbid ⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) Fn 𝑁 ∧ 𝑎 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 ↔ ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ) )
198 194 195 197 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 ↔ ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ) )
199 198 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 ↔ ¬ 𝑎 ∈ dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ∖ I ) ) )
200 191 199 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) = 𝑎 )
201 200 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) = ( 𝑑 ‘ 𝑎 ) )
202 201 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
203 iffalse ⊢ ( ¬ 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
204 203 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
205 202 204 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) ∧ ¬ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
206 174 205 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
207 iffalse ⊢ ( ¬ 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
208 207 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
209 206 208 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑐 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
210 154 209 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
211 210 3adant3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
212 211 mpoeq3dva ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
213 140 212 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
214 213 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
215 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝑑 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑐 ) )
216 215 oveq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
217 iftrue ⊢ ( 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) )
218 216 217 eqtr4d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
219 fveq2 ⊢ ( 𝑎 = 𝑓 → ( 𝑑 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑓 ) )
220 219 oveq1d ⊢ ( 𝑎 = 𝑓 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
221 iftrue ⊢ ( 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) )
222 220 221 eqtr4d ⊢ ( 𝑎 = 𝑓 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
223 222 adantl ⊢ ( ( ¬ 𝑎 = 𝑐 ∧ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
224 iffalse ⊢ ( ¬ 𝑎 = 𝑓 → if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) )
225 224 eqcomd ⊢ ( ¬ 𝑎 = 𝑓 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
226 225 adantl ⊢ ( ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
227 223 226 pm2.61dan ⊢ ( ¬ 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
228 iffalse ⊢ ( ¬ 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
229 227 228 eqtr4d ⊢ ( ¬ 𝑎 = 𝑐 → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
230 218 229 pm2.61i ⊢ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) )
231 230 a1i ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) = if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
232 231 mpoeq3ia ⊢ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) )
233 232 fveq2i ⊢ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
234 233 fveq2i ⊢ ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
235 234 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , ( ( 𝑑 ‘ 𝑐 ) 𝐹 𝑏 ) , if ( 𝑎 = 𝑓 , ( ( 𝑑 ‘ 𝑓 ) 𝐹 𝑏 ) , ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) ) )
236 139 214 235 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
237 fveq1 ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝑒 ‘ 𝑎 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) )
238 237 fveq2d ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) = ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) )
239 238 oveq1d ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) = ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) )
240 239 mpoeq3dv ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) )
241 240 fveqeq2d ⊢ ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ↔ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
242 236 241 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ∧ 𝑐 ≠ 𝑓 ) ) → ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
243 242 expr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ) → ( 𝑐 ≠ 𝑓 → ( 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) ) )
244 243 impd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ) ) → ( ( 𝑐 ≠ 𝑓 ∧ 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
245 244 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → ( ∃ 𝑐 ∈ 𝑁 ∃ 𝑓 ∈ 𝑁 ( 𝑐 ≠ 𝑓 ∧ 𝑒 = ( ( pmTrsp ‘ 𝑁 ) ‘ { 𝑐 , 𝑓 } ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
246 113 245 syl5 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ) → ( 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) ) )
247 246 3impia ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 : 𝑁 ⟶ 𝑁 ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
248 111 247 syl3an2 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ ( 𝑒 ‘ 𝑎 ) ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
249 110 248 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
250 249 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) )
251 fveq2 ⊢ ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
252 251 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
253 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
254 58 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑅 ∈ Ring )
255 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
256 255 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
257 66 3 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
258 44 257 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
259 256 258 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
260 259 93 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ∈ 𝐾 )
261 59 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝐷 : 𝐵 ⟶ 𝐾 )
262 simp13 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝐹 ∈ 𝐵 )
263 261 262 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ 𝐾 )
264 3 7 253 254 260 263 ringmneg1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
265 66 7 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
266 44 43 265 mhmlin ⊢ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) ) )
267 256 93 95 266 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) ) )
268 45 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑁 ∈ Fin )
269 simp3 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) )
270 46 44 50 pmtrodpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
271 268 269 270 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → 𝑒 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) )
272 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
273 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
274 272 273 5 44 253 zrhpsgnodpm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ( ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) = ( ( invg ‘ 𝑅 ) ‘ 1 ) )
275 254 268 271 274 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) = ( ( invg ‘ 𝑅 ) ‘ 1 ) )
276 275 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑒 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( invg ‘ 𝑅 ) ‘ 1 ) ) )
277 3 7 5 253 254 260 rngnegr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( ( invg ‘ 𝑅 ) ‘ 1 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) )
278 267 276 277 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) )
279 278 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
280 264 279 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
281 280 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
282 250 252 281 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) ∧ 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑒 ∈ ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝑑 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑑 ) · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 𝑑 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑒 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
283 simp2 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
284 46 44 elsymgbas ⊢ ( 𝑁 ∈ Fin → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
285 45 284 syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
286 283 285 mpbird ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
287 20 27 34 41 42 43 44 49 52 57 92 282 286 mndind ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) 𝐹 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ 𝐹 ) ) )