MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetunilem7 Structured version   Visualization version   GIF version

Theorem mdetunilem7 22564
Description: Lemma for mdetuni 22568. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
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
Ref Expression
mdetunilem7 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝐵,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝐾,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝑁,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝐷,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥, · ,𝑦,𝑧,𝑤   + ,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   0 ,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   1 ,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   𝑥,𝑅,𝑦,𝑧,𝑤   𝐴,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   𝑥,𝐸,𝑦,𝑧,𝑤   𝑥,𝐹,𝑦,𝑧,𝑤   𝐸,𝑎,𝑏   𝐹,𝑎,𝑏
Allowed substitution hints:   𝑅(𝑎,𝑏)   · (𝑎,𝑏)

Proof of Theorem mdetunilem7
Dummy variables 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq1 6895 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
21oveq1d 7434 . . . . 5 (𝑐 = 𝑑 → ((𝑐𝑎)𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
32mpoeq3dv 7499 . . . 4 (𝑐 = 𝑑 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))
43fveq2d 6900 . . 3 (𝑐 = 𝑑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))
5 fveq2 6896 . . . 4 (𝑐 = 𝑑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑))
65oveq1d 7434 . . 3 (𝑐 = 𝑑 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)))
74, 6eqeq12d 2741 . 2 (𝑐 = 𝑑 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
8 fveq1 6895 . . . . . 6 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑐𝑎) = ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎))
98oveq1d 7434 . . . . 5 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝑐𝑎)𝐹𝑏) = (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))
109mpoeq3dv 7499 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)))
1110fveq2d 6900 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))))
12 fveq2 6896 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
1312oveq1d 7434 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
1411, 13eqeq12d 2741 . 2 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹))))
15 fveq1 6895 . . . . . 6 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑐𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
1615oveq1d 7434 . . . . 5 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝑐𝑎)𝐹𝑏) = (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))
1716mpoeq3dv 7499 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)))
1817fveq2d 6900 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))))
19 fveq2 6896 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))))
2019oveq1d 7434 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
2118, 20eqeq12d 2741 . 2 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹))))
22 fveq1 6895 . . . . . 6 (𝑐 = 𝐸 → (𝑐𝑎) = (𝐸𝑎))
2322oveq1d 7434 . . . . 5 (𝑐 = 𝐸 → ((𝑐𝑎)𝐹𝑏) = ((𝐸𝑎)𝐹𝑏))
2423mpoeq3dv 7499 . . . 4 (𝑐 = 𝐸 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏)))
2524fveq2d 6900 . . 3 (𝑐 = 𝐸 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))))
26 fveq2 6896 . . . 4 (𝑐 = 𝐸 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸))
2726oveq1d 7434 . . 3 (𝑐 = 𝐸 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
2825, 27eqeq12d 2741 . 2 (𝑐 = 𝐸 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹))))
29 eqid 2725 . 2 (0g‘(SymGrp‘𝑁)) = (0g‘(SymGrp‘𝑁))
30 eqid 2725 . 2 (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
31 eqid 2725 . 2 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
32 mdetuni.n . . . 4 (𝜑𝑁 ∈ Fin)
33323ad2ant1 1130 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑁 ∈ Fin)
34 eqid 2725 . . . 4 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3534symggrp 19367 . . 3 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
36 grpmnd 18905 . . 3 ((SymGrp‘𝑁) ∈ Grp → (SymGrp‘𝑁) ∈ Mnd)
3733, 35, 363syl 18 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (SymGrp‘𝑁) ∈ Mnd)
38 eqid 2725 . . . 4 ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
3938, 34, 31symgtrf 19436 . . 3 ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
4039a1i 11 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
41 eqid 2725 . . . . . 6 (mrCls‘(SubMnd‘(SymGrp‘𝑁))) = (mrCls‘(SubMnd‘(SymGrp‘𝑁)))
4238, 34, 31, 41symggen2 19438 . . . . 5 (𝑁 ∈ Fin → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4332, 42syl 17 . . . 4 (𝜑 → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4443eqcomd 2731 . . 3 (𝜑 → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
45443ad2ant1 1130 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
46 mdetuni.r . . . . 5 (𝜑𝑅 ∈ Ring)
47463ad2ant1 1130 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑅 ∈ Ring)
48 mdetuni.ff . . . . . 6 (𝜑𝐷:𝐵𝐾)
49483ad2ant1 1130 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐷:𝐵𝐾)
50 simp3 1135 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹𝐵)
5149, 50ffvelcdmd 7094 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷𝐹) ∈ 𝐾)
52 mdetuni.k . . . . 5 𝐾 = (Base‘𝑅)
53 mdetuni.tg . . . . 5 · = (.r𝑅)
54 mdetuni.1r . . . . 5 1 = (1r𝑅)
5552, 53, 54ringlidm 20217 . . . 4 ((𝑅 ∈ Ring ∧ (𝐷𝐹) ∈ 𝐾) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
5647, 51, 55syl2anc 582 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
57 zrhpsgnmhm 21533 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
5846, 32, 57syl2anc 582 . . . . . 6 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
59 eqid 2725 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
6059, 54ringidval 20135 . . . . . . 7 1 = (0g‘(mulGrp‘𝑅))
6129, 60mhm0 18754 . . . . . 6 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6258, 61syl 17 . . . . 5 (𝜑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
63623ad2ant1 1130 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6463oveq1d 7434 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)) = ( 1 · (𝐷𝐹)))
6534symgid 19368 . . . . . . . . . . . 12 (𝑁 ∈ Fin → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6632, 65syl 17 . . . . . . . . . . 11 (𝜑 → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
67663ad2ant1 1130 . . . . . . . . . 10 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
68673ad2ant1 1130 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6968fveq1d 6898 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
70 simp2 1134 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
71 fvresi 7182 . . . . . . . . 9 (𝑎𝑁 → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7270, 71syl 17 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7369, 72eqtr3d 2767 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ((0g‘(SymGrp‘𝑁))‘𝑎) = 𝑎)
7473oveq1d 7434 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏) = (𝑎𝐹𝑏))
7574mpoeq3dva 7497 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
76 mdetuni.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
77 mdetuni.b . . . . . . . . 9 𝐵 = (Base‘𝐴)
7876, 52, 77matbas2i 22368 . . . . . . . 8 (𝐹𝐵𝐹 ∈ (𝐾m (𝑁 × 𝑁)))
79783ad2ant3 1132 . . . . . . 7 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 ∈ (𝐾m (𝑁 × 𝑁)))
80 elmapi 8868 . . . . . . 7 (𝐹 ∈ (𝐾m (𝑁 × 𝑁)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
81 ffn 6723 . . . . . . 7 (𝐹:(𝑁 × 𝑁)⟶𝐾𝐹 Fn (𝑁 × 𝑁))
8279, 80, 813syl 18 . . . . . 6 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 Fn (𝑁 × 𝑁))
83 fnov 7552 . . . . . 6 (𝐹 Fn (𝑁 × 𝑁) ↔ 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8482, 83sylib 217 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8575, 84eqtr4d 2768 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = 𝐹)
8685fveq2d 6900 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = (𝐷𝐹))
8756, 64, 863eqtr4rd 2776 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
88 simp2 1134 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑑 ∈ (Base‘(SymGrp‘𝑁)))
8939sseli 3972 . . . . . . . . . . . . 13 (𝑒 ∈ ran (pmTrsp‘𝑁) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
90893ad2ant3 1132 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
9134, 31, 30symgov 19350 . . . . . . . . . . . 12 ((𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9288, 90, 91syl2anc 582 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9392fveq1d 6898 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
94933ad2ant1 1130 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
9534, 31symgbasf1o 19341 . . . . . . . . . . . 12 (𝑒 ∈ (Base‘(SymGrp‘𝑁)) → 𝑒:𝑁1-1-onto𝑁)
96 f1of 6838 . . . . . . . . . . . 12 (𝑒:𝑁1-1-onto𝑁𝑒:𝑁𝑁)
9790, 95, 963syl 18 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒:𝑁𝑁)
98973ad2ant1 1130 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑒:𝑁𝑁)
99 simp2 1134 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
100 fvco3 6996 . . . . . . . . . 10 ((𝑒:𝑁𝑁𝑎𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10198, 99, 100syl2anc 582 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10294, 101eqtrd 2765 . . . . . . . 8 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
103102oveq1d 7434 . . . . . . 7 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏) = ((𝑑‘(𝑒𝑎))𝐹𝑏))
104103mpoeq3dva 7497 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)))
105104fveq2d 6900 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))))
10634, 31symgbasf 19342 . . . . . 6 (𝑑 ∈ (Base‘(SymGrp‘𝑁)) → 𝑑:𝑁𝑁)
107 eqid 2725 . . . . . . . . 9 (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
108107, 38pmtrrn2 19427 . . . . . . . 8 (𝑒 ∈ ran (pmTrsp‘𝑁) → ∃𝑐𝑁𝑓𝑁 (𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})))
109 mdetuni.0g . . . . . . . . . . . . . 14 0 = (0g𝑅)
110 mdetuni.pg . . . . . . . . . . . . . 14 + = (+g𝑅)
111 mdetuni.al . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
112 mdetuni.li . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
113 mdetuni.sc . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
114 simpll1 1209 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝜑)
115 df-3an 1086 . . . . . . . . . . . . . . . 16 ((𝑐𝑁𝑓𝑁𝑐𝑓) ↔ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓))
116115biimpri 227 . . . . . . . . . . . . . . 15 (((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓) → (𝑐𝑁𝑓𝑁𝑐𝑓))
117116adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑐𝑁𝑓𝑁𝑐𝑓))
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
119118adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
120119ad2antrr 724 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
121 simpllr 774 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑑:𝑁𝑁)
122 simprlr 778 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
123122adantr 479 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑓𝑁)
124121, 123ffvelcdmd 7094 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑓) ∈ 𝑁)
125 simpr 483 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑏𝑁)
126120, 124, 125fovcdmd 7593 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑓)𝐹𝑏) ∈ 𝐾)
127 simprll 777 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
128127adantr 479 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑐𝑁)
129121, 128ffvelcdmd 7094 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑐) ∈ 𝑁)
130120, 129, 125fovcdmd 7593 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑐)𝐹𝑏) ∈ 𝐾)
131126, 130jca 510 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (((𝑑𝑓)𝐹𝑏) ∈ 𝐾 ∧ ((𝑑𝑐)𝐹𝑏) ∈ 𝐾))
132118ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
1331323ad2ant1 1130 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
134 simp1lr 1234 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑑:𝑁𝑁)
135 simp2 1134 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
136134, 135ffvelcdmd 7094 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → (𝑑𝑎) ∈ 𝑁)
137 simp3 1135 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
138133, 136, 137fovcdmd 7593 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) ∈ 𝐾)
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 22563 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
140 simpl1 1188 . . . . . . . . . . . . . . 15 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝜑)
141 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑐 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐))
14232adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑁 ∈ Fin)
143 simprll 777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
144 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
145 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑓)
146107pmtrprfv 19420 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ Fin ∧ (𝑐𝑁𝑓𝑁𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
147142, 143, 144, 145, 146syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
148147adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
149141, 148sylan9eqr 2787 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑓)
150149fveq2d 6900 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑓))
151150oveq1d 7434 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
152 iftrue 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
153152adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
154151, 153eqtr4d 2768 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
155 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑓 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓))
156 prcom 4738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑐, 𝑓} = {𝑓, 𝑐}
157156fveq2i 6899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) = ((pmTrsp‘𝑁)‘{𝑓, 𝑐})
158157fveq1i 6897 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓)
15932ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
160 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑐𝑁𝑓𝑁))
161160simprd 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑁)
162160simpld 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑁)
163 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑓)
164163necomd 2985 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑐)
165107pmtrprfv 19420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ Fin ∧ (𝑓𝑁𝑐𝑁𝑓𝑐)) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
166159, 161, 162, 164, 165syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
167158, 166eqtrid 2777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = 𝑐)
168155, 167sylan9eqr 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑐)
169168fveq2d 6900 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑐))
170169oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
171 iftrue 4536 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
172171adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
173170, 172eqtr4d 2768 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
174173adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
175 vex 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑎 ∈ V
176175elpr 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ {𝑐, 𝑓} ↔ (𝑎 = 𝑐𝑎 = 𝑓))
177176notbii 319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ {𝑐, 𝑓} ↔ ¬ (𝑎 = 𝑐𝑎 = 𝑓))
178 ioran 981 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (𝑎 = 𝑐𝑎 = 𝑓) ↔ (¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓))
179177, 178sylbbr 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
180179adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
181 prssi 4826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐𝑁𝑓𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
183 pr2ne 10029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐𝑁𝑓𝑁) → ({𝑐, 𝑓} ≈ 2o𝑐𝑓))
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ({𝑐, 𝑓} ≈ 2o𝑐𝑓))
185163, 184mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ≈ 2o)
186107pmtrmvd 19423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
187159, 182, 185, 186syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
188187eleq2d 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ 𝑎 ∈ {𝑐, 𝑓}))
189188notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
190189ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
191180, 190mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ))
192107pmtrf 19422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
193159, 182, 185, 192syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
194193ffnd 6724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
195 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑎𝑁)
196 fnelnfp 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) ≠ 𝑎))
197196necon2bbid 2973 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
198194, 195, 197syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
199198ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
200191, 199mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎)
201200fveq2d 6900 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑎))
202201oveq1d 7434 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
203 iffalse 4539 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
204203adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
205202, 204eqtr4d 2768 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
206174, 205pm2.61dan 811 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
207 iffalse 4539 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
208207adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
209206, 208eqtr4d 2768 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
210154, 209pm2.61dan 811 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
2112103adant3 1129 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
212211mpoeq3dva 7497 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
213140, 212sylan 578 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
214213fveq2d 6900 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
215 fveq2 6896 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑑𝑎) = (𝑑𝑐))
216215oveq1d 7434 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
217 iftrue 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑐)𝐹𝑏))
218216, 217eqtr4d 2768 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
219 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑓 → (𝑑𝑎) = (𝑑𝑓))
220219oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
221 iftrue 4536 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑓)𝐹𝑏))
222220, 221eqtr4d 2768 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
223222adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
224 iffalse 4539 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
225224eqcomd 2731 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
226225adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
227223, 226pm2.61dan 811 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
228 iffalse 4539 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
229227, 228eqtr4d 2768 . . . . . . . . . . . . . . . . . . 19 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
230218, 229pm2.61i 182 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
231230a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
232231mpoeq3ia 7498 . . . . . . . . . . . . . . . 16 (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
233232fveq2i 6899 . . . . . . . . . . . . . . 15 (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
234233fveq2i 6899 . . . . . . . . . . . . . 14 ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
235234a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
236139, 214, 2353eqtr4d 2775 . . . . . . . . . . . 12 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
237 fveq1 6895 . . . . . . . . . . . . . . . 16 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑒𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))
238237fveq2d 6900 . . . . . . . . . . . . . . 15 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑑‘(𝑒𝑎)) = (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)))
239238oveq1d 7434 . . . . . . . . . . . . . 14 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝑑‘(𝑒𝑎))𝐹𝑏) = ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))
240239mpoeq3dv 7499 . . . . . . . . . . . . 13 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)))
241240fveqeq2d 6904 . . . . . . . . . . . 12 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
242236, 241syl5ibrcom 246 . . . . . . . . . . 11 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
243242expr 455 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → (𝑐𝑓 → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))))
244243impd 409 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → ((𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
245244rexlimdvva 3201 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (∃𝑐𝑁𝑓𝑁 (𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
246108, 245syl5 34 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (𝑒 ∈ ran (pmTrsp‘𝑁) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
2472463impia 1114 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
248106, 247syl3an2 1161 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
249105, 248eqtrd 2765 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
250249adantr 479 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
251 fveq2 6896 . . . 4 ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
252251adantl 480 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
253 eqid 2725 . . . . . 6 (invg𝑅) = (invg𝑅)
254473ad2ant1 1130 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑅 ∈ Ring)
255583ad2ant1 1130 . . . . . . . . 9 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2562553ad2ant1 1130 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
25759, 52mgpbas 20092 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
25831, 257mhmf 18749 . . . . . . . 8 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
259256, 258syl 17 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
260259, 88ffvelcdmd 7094 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) ∈ 𝐾)
261493ad2ant1 1130 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐷:𝐵𝐾)
262 simp13 1202 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐹𝐵)
263261, 262ffvelcdmd 7094 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷𝐹) ∈ 𝐾)
26452, 53, 253, 254, 260, 263ringmneg1 20252 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
26559, 53mgpplusg 20090 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
26631, 30, 265mhmlin 18753 . . . . . . . 8 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
267256, 88, 90, 266syl3anc 1368 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
268333ad2ant1 1130 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑁 ∈ Fin)
269 simp3 1135 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ran (pmTrsp‘𝑁))
27034, 31, 38pmtrodpm 21546 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
271268, 269, 270syl2anc 582 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
272 eqid 2725 . . . . . . . . . 10 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
273 eqid 2725 . . . . . . . . . 10 (pmSgn‘𝑁) = (pmSgn‘𝑁)
274272, 273, 54, 31, 253zrhpsgnodpm 21541 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
275254, 268, 271, 274syl3anc 1368 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
276275oveq2d 7435 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )))
27752, 53, 54, 253, 254, 260ringnegr 20251 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )) = ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)))
278267, 276, 2773eqtrrd 2770 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
279278oveq1d 7434 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
280264, 279eqtr3d 2767 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
281280adantr 479 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
282250, 252, 2813eqtrd 2769 . 2 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
283 simp2 1134 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸:𝑁1-1-onto𝑁)
28434, 31elsymgbas 19340 . . . 4 (𝑁 ∈ Fin → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
28533, 284syl 17 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
286283, 285mpbird 256 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸 ∈ (Base‘(SymGrp‘𝑁)))
2877, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 282, 286mndind 18788 1 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  cdif 3941  wss 3944  ifcif 4530  {csn 4630  {cpr 4632   class class class wbr 5149   I cid 5575   × cxp 5676  dom cdm 5678  ran crn 5679  cres 5680  ccom 5682   Fn wfn 6544  wf 6545  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  cmpo 7421  f cof 7683  2oc2o 8481  m cmap 8845  cen 8961  Fincfn 8964  Basecbs 17183  +gcplusg 17236  .rcmulr 17237  0gc0g 17424  mrClscmrc 17566  Mndcmnd 18697   MndHom cmhm 18741  SubMndcsubmnd 18742  Grpcgrp 18898  invgcminusg 18899  SymGrpcsymg 19333  pmTrspcpmtr 19408  pmSgncpsgn 19456  pmEvencevpm 19457  mulGrpcmgp 20086  1rcur 20133  Ringcrg 20185  ℤRHomczrh 21442   Mat cmat 22351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-addf 11219  ax-mulf 11220
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-xor 1505  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-ot 4639  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-tpos 8232  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-sup 9467  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12506  df-xnn0 12578  df-z 12592  df-dec 12711  df-uz 12856  df-rp 13010  df-fz 13520  df-fzo 13663  df-seq 14003  df-exp 14063  df-hash 14326  df-word 14501  df-lsw 14549  df-concat 14557  df-s1 14582  df-substr 14627  df-pfx 14657  df-splice 14736  df-reverse 14745  df-s2 14835  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-starv 17251  df-sca 17252  df-vsca 17253  df-ip 17254  df-tset 17255  df-ple 17256  df-ds 17258  df-unif 17259  df-hom 17260  df-cco 17261  df-0g 17426  df-gsum 17427  df-prds 17432  df-pws 17434  df-mre 17569  df-mrc 17570  df-acs 17572  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18743  df-submnd 18744  df-efmnd 18829  df-grp 18901  df-minusg 18902  df-mulg 19032  df-subg 19086  df-ghm 19176  df-gim 19222  df-oppg 19309  df-symg 19334  df-pmtr 19409  df-psgn 19458  df-evpm 19459  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-cring 20188  df-oppr 20285  df-dvdsr 20308  df-unit 20309  df-invr 20339  df-dvr 20352  df-rhm 20423  df-subrng 20495  df-subrg 20520  df-drng 20638  df-sra 21070  df-rgmod 21071  df-cnfld 21297  df-zring 21390  df-zrh 21446  df-dsmm 21683  df-frlm 21698  df-mat 22352
This theorem is referenced by:  mdetunilem8  22565
  Copyright terms: Public domain W3C validator