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

Theorem mdetunilem7 22624
Description: Lemma for mdetuni 22628. (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 6905 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
21oveq1d 7446 . . . . 5 (𝑐 = 𝑑 → ((𝑐𝑎)𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
32mpoeq3dv 7512 . . . 4 (𝑐 = 𝑑 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))
43fveq2d 6910 . . 3 (𝑐 = 𝑑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))
5 fveq2 6906 . . . 4 (𝑐 = 𝑑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑))
65oveq1d 7446 . . 3 (𝑐 = 𝑑 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)))
74, 6eqeq12d 2753 . 2 (𝑐 = 𝑑 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
8 fveq1 6905 . . . . . 6 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑐𝑎) = ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎))
98oveq1d 7446 . . . . 5 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝑐𝑎)𝐹𝑏) = (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))
109mpoeq3dv 7512 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)))
1110fveq2d 6910 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))))
12 fveq2 6906 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
1312oveq1d 7446 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
1411, 13eqeq12d 2753 . 2 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹))))
15 fveq1 6905 . . . . . 6 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑐𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
1615oveq1d 7446 . . . . 5 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝑐𝑎)𝐹𝑏) = (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))
1716mpoeq3dv 7512 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)))
1817fveq2d 6910 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))))
19 fveq2 6906 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))))
2019oveq1d 7446 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
2118, 20eqeq12d 2753 . 2 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹))))
22 fveq1 6905 . . . . . 6 (𝑐 = 𝐸 → (𝑐𝑎) = (𝐸𝑎))
2322oveq1d 7446 . . . . 5 (𝑐 = 𝐸 → ((𝑐𝑎)𝐹𝑏) = ((𝐸𝑎)𝐹𝑏))
2423mpoeq3dv 7512 . . . 4 (𝑐 = 𝐸 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏)))
2524fveq2d 6910 . . 3 (𝑐 = 𝐸 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))))
26 fveq2 6906 . . . 4 (𝑐 = 𝐸 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸))
2726oveq1d 7446 . . 3 (𝑐 = 𝐸 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
2825, 27eqeq12d 2753 . 2 (𝑐 = 𝐸 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹))))
29 eqid 2737 . 2 (0g‘(SymGrp‘𝑁)) = (0g‘(SymGrp‘𝑁))
30 eqid 2737 . 2 (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
31 eqid 2737 . 2 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
32 mdetuni.n . . . 4 (𝜑𝑁 ∈ Fin)
33323ad2ant1 1134 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑁 ∈ Fin)
34 eqid 2737 . . . 4 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3534symggrp 19418 . . 3 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
36 grpmnd 18958 . . 3 ((SymGrp‘𝑁) ∈ Grp → (SymGrp‘𝑁) ∈ Mnd)
3733, 35, 363syl 18 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (SymGrp‘𝑁) ∈ Mnd)
38 eqid 2737 . . . 4 ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
3938, 34, 31symgtrf 19487 . . 3 ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
4039a1i 11 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
41 eqid 2737 . . . . . 6 (mrCls‘(SubMnd‘(SymGrp‘𝑁))) = (mrCls‘(SubMnd‘(SymGrp‘𝑁)))
4238, 34, 31, 41symggen2 19489 . . . . 5 (𝑁 ∈ Fin → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4332, 42syl 17 . . . 4 (𝜑 → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4443eqcomd 2743 . . 3 (𝜑 → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
45443ad2ant1 1134 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
46 mdetuni.r . . . . 5 (𝜑𝑅 ∈ Ring)
47463ad2ant1 1134 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑅 ∈ Ring)
48 mdetuni.ff . . . . . 6 (𝜑𝐷:𝐵𝐾)
49483ad2ant1 1134 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐷:𝐵𝐾)
50 simp3 1139 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹𝐵)
5149, 50ffvelcdmd 7105 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷𝐹) ∈ 𝐾)
52 mdetuni.k . . . . 5 𝐾 = (Base‘𝑅)
53 mdetuni.tg . . . . 5 · = (.r𝑅)
54 mdetuni.1r . . . . 5 1 = (1r𝑅)
5552, 53, 54ringlidm 20266 . . . 4 ((𝑅 ∈ Ring ∧ (𝐷𝐹) ∈ 𝐾) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
5647, 51, 55syl2anc 584 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
57 zrhpsgnmhm 21602 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
5846, 32, 57syl2anc 584 . . . . . 6 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
59 eqid 2737 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
6059, 54ringidval 20180 . . . . . . 7 1 = (0g‘(mulGrp‘𝑅))
6129, 60mhm0 18807 . . . . . 6 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6258, 61syl 17 . . . . 5 (𝜑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
63623ad2ant1 1134 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6463oveq1d 7446 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)) = ( 1 · (𝐷𝐹)))
6534symgid 19419 . . . . . . . . . . . 12 (𝑁 ∈ Fin → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6632, 65syl 17 . . . . . . . . . . 11 (𝜑 → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
67663ad2ant1 1134 . . . . . . . . . 10 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
68673ad2ant1 1134 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6968fveq1d 6908 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
70 simp2 1138 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
71 fvresi 7193 . . . . . . . . 9 (𝑎𝑁 → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7270, 71syl 17 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7369, 72eqtr3d 2779 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ((0g‘(SymGrp‘𝑁))‘𝑎) = 𝑎)
7473oveq1d 7446 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏) = (𝑎𝐹𝑏))
7574mpoeq3dva 7510 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
76 mdetuni.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
77 mdetuni.b . . . . . . . . 9 𝐵 = (Base‘𝐴)
7876, 52, 77matbas2i 22428 . . . . . . . 8 (𝐹𝐵𝐹 ∈ (𝐾m (𝑁 × 𝑁)))
79783ad2ant3 1136 . . . . . . 7 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 ∈ (𝐾m (𝑁 × 𝑁)))
80 elmapi 8889 . . . . . . 7 (𝐹 ∈ (𝐾m (𝑁 × 𝑁)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
81 ffn 6736 . . . . . . 7 (𝐹:(𝑁 × 𝑁)⟶𝐾𝐹 Fn (𝑁 × 𝑁))
8279, 80, 813syl 18 . . . . . 6 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 Fn (𝑁 × 𝑁))
83 fnov 7564 . . . . . 6 (𝐹 Fn (𝑁 × 𝑁) ↔ 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8482, 83sylib 218 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8575, 84eqtr4d 2780 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = 𝐹)
8685fveq2d 6910 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = (𝐷𝐹))
8756, 64, 863eqtr4rd 2788 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
88 simp2 1138 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑑 ∈ (Base‘(SymGrp‘𝑁)))
8939sseli 3979 . . . . . . . . . . . . 13 (𝑒 ∈ ran (pmTrsp‘𝑁) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
90893ad2ant3 1136 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
9134, 31, 30symgov 19401 . . . . . . . . . . . 12 ((𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9288, 90, 91syl2anc 584 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9392fveq1d 6908 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
94933ad2ant1 1134 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
9534, 31symgbasf1o 19392 . . . . . . . . . . . 12 (𝑒 ∈ (Base‘(SymGrp‘𝑁)) → 𝑒:𝑁1-1-onto𝑁)
96 f1of 6848 . . . . . . . . . . . 12 (𝑒:𝑁1-1-onto𝑁𝑒:𝑁𝑁)
9790, 95, 963syl 18 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒:𝑁𝑁)
98973ad2ant1 1134 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑒:𝑁𝑁)
99 simp2 1138 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
100 fvco3 7008 . . . . . . . . . 10 ((𝑒:𝑁𝑁𝑎𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10198, 99, 100syl2anc 584 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10294, 101eqtrd 2777 . . . . . . . 8 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
103102oveq1d 7446 . . . . . . 7 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏) = ((𝑑‘(𝑒𝑎))𝐹𝑏))
104103mpoeq3dva 7510 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)))
105104fveq2d 6910 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))))
10634, 31symgbasf 19393 . . . . . 6 (𝑑 ∈ (Base‘(SymGrp‘𝑁)) → 𝑑:𝑁𝑁)
107 eqid 2737 . . . . . . . . 9 (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
108107, 38pmtrrn2 19478 . . . . . . . 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 1213 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝜑)
115 df-3an 1089 . . . . . . . . . . . . . . . 16 ((𝑐𝑁𝑓𝑁𝑐𝑓) ↔ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓))
116115biimpri 228 . . . . . . . . . . . . . . 15 (((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓) → (𝑐𝑁𝑓𝑁𝑐𝑓))
117116adantl 481 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑐𝑁𝑓𝑁𝑐𝑓))
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
119118adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
120119ad2antrr 726 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
121 simpllr 776 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑑:𝑁𝑁)
122 simprlr 780 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
123122adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑓𝑁)
124121, 123ffvelcdmd 7105 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑓) ∈ 𝑁)
125 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑏𝑁)
126120, 124, 125fovcdmd 7605 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑓)𝐹𝑏) ∈ 𝐾)
127 simprll 779 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
128127adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑐𝑁)
129121, 128ffvelcdmd 7105 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑐) ∈ 𝑁)
130120, 129, 125fovcdmd 7605 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑐)𝐹𝑏) ∈ 𝐾)
131126, 130jca 511 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (((𝑑𝑓)𝐹𝑏) ∈ 𝐾 ∧ ((𝑑𝑐)𝐹𝑏) ∈ 𝐾))
132118ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
1331323ad2ant1 1134 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
134 simp1lr 1238 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑑:𝑁𝑁)
135 simp2 1138 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
136134, 135ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → (𝑑𝑎) ∈ 𝑁)
137 simp3 1139 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
138133, 136, 137fovcdmd 7605 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) ∈ 𝐾)
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 22623 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
140 simpl1 1192 . . . . . . . . . . . . . . 15 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝜑)
141 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑐 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐))
14232adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑁 ∈ Fin)
143 simprll 779 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
144 simprlr 780 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
145 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑓)
146107pmtrprfv 19471 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ Fin ∧ (𝑐𝑁𝑓𝑁𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
147142, 143, 144, 145, 146syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
148147adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
149141, 148sylan9eqr 2799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑓)
150149fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑓))
151150oveq1d 7446 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
152 iftrue 4531 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
153152adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
154151, 153eqtr4d 2780 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
155 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑓 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓))
156 prcom 4732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑐, 𝑓} = {𝑓, 𝑐}
157156fveq2i 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) = ((pmTrsp‘𝑁)‘{𝑓, 𝑐})
158157fveq1i 6907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓)
15932ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
160 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑐𝑁𝑓𝑁))
161160simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑁)
162160simpld 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑁)
163 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑓)
164163necomd 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑐)
165107pmtrprfv 19471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ Fin ∧ (𝑓𝑁𝑐𝑁𝑓𝑐)) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
166159, 161, 162, 164, 165syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
167158, 166eqtrid 2789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = 𝑐)
168155, 167sylan9eqr 2799 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑐)
169168fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑐))
170169oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
171 iftrue 4531 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
172171adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
173170, 172eqtr4d 2780 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
174173adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
175 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑎 ∈ V
176175elpr 4650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ {𝑐, 𝑓} ↔ (𝑎 = 𝑐𝑎 = 𝑓))
177176notbii 320 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ {𝑐, 𝑓} ↔ ¬ (𝑎 = 𝑐𝑎 = 𝑓))
178 ioran 986 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (𝑎 = 𝑐𝑎 = 𝑓) ↔ (¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓))
179177, 178sylbbr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
180179adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
181 prssi 4821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐𝑁𝑓𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
183 pr2ne 10044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐𝑁𝑓𝑁) → ({𝑐, 𝑓} ≈ 2o𝑐𝑓))
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ({𝑐, 𝑓} ≈ 2o𝑐𝑓))
185163, 184mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ≈ 2o)
186107pmtrmvd 19474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
187159, 182, 185, 186syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
188187eleq2d 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ 𝑎 ∈ {𝑐, 𝑓}))
189188notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
190189ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
191180, 190mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ))
192107pmtrf 19473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
193159, 182, 185, 192syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
194193ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
195 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑎𝑁)
196 fnelnfp 7197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) ≠ 𝑎))
197196necon2bbid 2984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
198194, 195, 197syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
199198ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
200191, 199mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎)
201200fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑎))
202201oveq1d 7446 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
203 iffalse 4534 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
204203adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
205202, 204eqtr4d 2780 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
206174, 205pm2.61dan 813 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
207 iffalse 4534 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
208207adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
209206, 208eqtr4d 2780 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
210154, 209pm2.61dan 813 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
2112103adant3 1133 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
212211mpoeq3dva 7510 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
213140, 212sylan 580 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
214213fveq2d 6910 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
215 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑑𝑎) = (𝑑𝑐))
216215oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
217 iftrue 4531 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑐)𝐹𝑏))
218216, 217eqtr4d 2780 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
219 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑓 → (𝑑𝑎) = (𝑑𝑓))
220219oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
221 iftrue 4531 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑓)𝐹𝑏))
222220, 221eqtr4d 2780 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
223222adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
224 iffalse 4534 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
225224eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
226225adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
227223, 226pm2.61dan 813 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
228 iffalse 4534 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
229227, 228eqtr4d 2780 . . . . . . . . . . . . . . . . . . 19 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
230218, 229pm2.61i 182 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
231230a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
232231mpoeq3ia 7511 . . . . . . . . . . . . . . . 16 (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
233232fveq2i 6909 . . . . . . . . . . . . . . 15 (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
234233fveq2i 6909 . . . . . . . . . . . . . 14 ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
235234a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
236139, 214, 2353eqtr4d 2787 . . . . . . . . . . . 12 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
237 fveq1 6905 . . . . . . . . . . . . . . . 16 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑒𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))
238237fveq2d 6910 . . . . . . . . . . . . . . 15 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑑‘(𝑒𝑎)) = (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)))
239238oveq1d 7446 . . . . . . . . . . . . . 14 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝑑‘(𝑒𝑎))𝐹𝑏) = ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))
240239mpoeq3dv 7512 . . . . . . . . . . . . 13 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)))
241240fveqeq2d 6914 . . . . . . . . . . . 12 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
242236, 241syl5ibrcom 247 . . . . . . . . . . 11 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
243242expr 456 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → (𝑐𝑓 → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))))
244243impd 410 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → ((𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
245244rexlimdvva 3213 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (∃𝑐𝑁𝑓𝑁 (𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
246108, 245syl5 34 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (𝑒 ∈ ran (pmTrsp‘𝑁) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
2472463impia 1118 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
248106, 247syl3an2 1165 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
249105, 248eqtrd 2777 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
250249adantr 480 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
251 fveq2 6906 . . . 4 ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
252251adantl 481 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
253 eqid 2737 . . . . . 6 (invg𝑅) = (invg𝑅)
254473ad2ant1 1134 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑅 ∈ Ring)
255583ad2ant1 1134 . . . . . . . . 9 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2562553ad2ant1 1134 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
25759, 52mgpbas 20142 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
25831, 257mhmf 18802 . . . . . . . 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 7105 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) ∈ 𝐾)
261493ad2ant1 1134 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐷:𝐵𝐾)
262 simp13 1206 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐹𝐵)
263261, 262ffvelcdmd 7105 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷𝐹) ∈ 𝐾)
26452, 53, 253, 254, 260, 263ringmneg1 20301 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
26559, 53mgpplusg 20141 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
26631, 30, 265mhmlin 18806 . . . . . . . 8 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
267256, 88, 90, 266syl3anc 1373 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
268333ad2ant1 1134 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑁 ∈ Fin)
269 simp3 1139 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ran (pmTrsp‘𝑁))
27034, 31, 38pmtrodpm 21615 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
271268, 269, 270syl2anc 584 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
272 eqid 2737 . . . . . . . . . 10 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
273 eqid 2737 . . . . . . . . . 10 (pmSgn‘𝑁) = (pmSgn‘𝑁)
274272, 273, 54, 31, 253zrhpsgnodpm 21610 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
275254, 268, 271, 274syl3anc 1373 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
276275oveq2d 7447 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )))
27752, 53, 54, 253, 254, 260ringnegr 20300 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )) = ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)))
278267, 276, 2773eqtrrd 2782 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
279278oveq1d 7446 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
280264, 279eqtr3d 2779 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
281280adantr 480 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
282250, 252, 2813eqtrd 2781 . 2 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
283 simp2 1138 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸:𝑁1-1-onto𝑁)
28434, 31elsymgbas 19391 . . . 4 (𝑁 ∈ Fin → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
28533, 284syl 17 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
286283, 285mpbird 257 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸 ∈ (Base‘(SymGrp‘𝑁)))
2877, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 282, 286mndind 18841 1 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  cdif 3948  wss 3951  ifcif 4525  {csn 4626  {cpr 4628   class class class wbr 5143   I cid 5577   × cxp 5683  dom cdm 5685  ran crn 5686  cres 5687  ccom 5689   Fn wfn 6556  wf 6557  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433  f cof 7695  2oc2o 8500  m cmap 8866  cen 8982  Fincfn 8985  Basecbs 17247  +gcplusg 17297  .rcmulr 17298  0gc0g 17484  mrClscmrc 17626  Mndcmnd 18747   MndHom cmhm 18794  SubMndcsubmnd 18795  Grpcgrp 18951  invgcminusg 18952  SymGrpcsymg 19386  pmTrspcpmtr 19459  pmSgncpsgn 19507  pmEvencevpm 19508  mulGrpcmgp 20137  1rcur 20178  Ringcrg 20230  ℤRHomczrh 21510   Mat cmat 22411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-addf 11234  ax-mulf 11235
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-word 14553  df-lsw 14601  df-concat 14609  df-s1 14634  df-substr 14679  df-pfx 14709  df-splice 14788  df-reverse 14797  df-s2 14887  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-0g 17486  df-gsum 17487  df-prds 17492  df-pws 17494  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-efmnd 18882  df-grp 18954  df-minusg 18955  df-mulg 19086  df-subg 19141  df-ghm 19231  df-gim 19277  df-oppg 19364  df-symg 19387  df-pmtr 19460  df-psgn 19509  df-evpm 19510  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-invr 20388  df-dvr 20401  df-rhm 20472  df-subrng 20546  df-subrg 20570  df-drng 20731  df-sra 21172  df-rgmod 21173  df-cnfld 21365  df-zring 21458  df-zrh 21514  df-dsmm 21752  df-frlm 21767  df-mat 22412
This theorem is referenced by:  mdetunilem8  22625
  Copyright terms: Public domain W3C validator