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

Theorem mdetunilem7 20364
Description: Lemma for mdetuni 20368. (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 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
mdetuni.sc (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
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 6157 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
21oveq1d 6630 . . . . 5 (𝑐 = 𝑑 → ((𝑐𝑎)𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
32mpt2eq3dv 6686 . . . 4 (𝑐 = 𝑑 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))
43fveq2d 6162 . . 3 (𝑐 = 𝑑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))
5 fveq2 6158 . . . 4 (𝑐 = 𝑑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑))
65oveq1d 6630 . . 3 (𝑐 = 𝑑 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)))
74, 6eqeq12d 2636 . 2 (𝑐 = 𝑑 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
8 fveq1 6157 . . . . . 6 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑐𝑎) = ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎))
98oveq1d 6630 . . . . 5 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝑐𝑎)𝐹𝑏) = (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))
109mpt2eq3dv 6686 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)))
1110fveq2d 6162 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))))
12 fveq2 6158 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
1312oveq1d 6630 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
1411, 13eqeq12d 2636 . 2 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹))))
15 fveq1 6157 . . . . . 6 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑐𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
1615oveq1d 6630 . . . . 5 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝑐𝑎)𝐹𝑏) = (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))
1716mpt2eq3dv 6686 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)))
1817fveq2d 6162 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))))
19 fveq2 6158 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))))
2019oveq1d 6630 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
2118, 20eqeq12d 2636 . 2 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹))))
22 fveq1 6157 . . . . . 6 (𝑐 = 𝐸 → (𝑐𝑎) = (𝐸𝑎))
2322oveq1d 6630 . . . . 5 (𝑐 = 𝐸 → ((𝑐𝑎)𝐹𝑏) = ((𝐸𝑎)𝐹𝑏))
2423mpt2eq3dv 6686 . . . 4 (𝑐 = 𝐸 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏)))
2524fveq2d 6162 . . 3 (𝑐 = 𝐸 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))))
26 fveq2 6158 . . . 4 (𝑐 = 𝐸 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸))
2726oveq1d 6630 . . 3 (𝑐 = 𝐸 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
2825, 27eqeq12d 2636 . 2 (𝑐 = 𝐸 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹))))
29 eqid 2621 . 2 (0g‘(SymGrp‘𝑁)) = (0g‘(SymGrp‘𝑁))
30 eqid 2621 . 2 (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
31 eqid 2621 . 2 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
32 mdetuni.n . . . 4 (𝜑𝑁 ∈ Fin)
33323ad2ant1 1080 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑁 ∈ Fin)
34 eqid 2621 . . . 4 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3534symggrp 17760 . . 3 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
36 grpmnd 17369 . . 3 ((SymGrp‘𝑁) ∈ Grp → (SymGrp‘𝑁) ∈ Mnd)
3733, 35, 363syl 18 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (SymGrp‘𝑁) ∈ Mnd)
38 eqid 2621 . . . 4 ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
3938, 34, 31symgtrf 17829 . . 3 ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
4039a1i 11 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
41 eqid 2621 . . . . . 6 (mrCls‘(SubMnd‘(SymGrp‘𝑁))) = (mrCls‘(SubMnd‘(SymGrp‘𝑁)))
4238, 34, 31, 41symggen2 17831 . . . . 5 (𝑁 ∈ Fin → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4332, 42syl 17 . . . 4 (𝜑 → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4443eqcomd 2627 . . 3 (𝜑 → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
45443ad2ant1 1080 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
46 mdetuni.r . . . . 5 (𝜑𝑅 ∈ Ring)
47463ad2ant1 1080 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑅 ∈ Ring)
48 mdetuni.ff . . . . . 6 (𝜑𝐷:𝐵𝐾)
49483ad2ant1 1080 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐷:𝐵𝐾)
50 simp3 1061 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹𝐵)
5149, 50ffvelrnd 6326 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷𝐹) ∈ 𝐾)
52 mdetuni.k . . . . 5 𝐾 = (Base‘𝑅)
53 mdetuni.tg . . . . 5 · = (.r𝑅)
54 mdetuni.1r . . . . 5 1 = (1r𝑅)
5552, 53, 54ringlidm 18511 . . . 4 ((𝑅 ∈ Ring ∧ (𝐷𝐹) ∈ 𝐾) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
5647, 51, 55syl2anc 692 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
57 zrhpsgnmhm 19870 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
5846, 32, 57syl2anc 692 . . . . . 6 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
59 eqid 2621 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
6059, 54ringidval 18443 . . . . . . 7 1 = (0g‘(mulGrp‘𝑅))
6129, 60mhm0 17283 . . . . . 6 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6258, 61syl 17 . . . . 5 (𝜑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
63623ad2ant1 1080 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6463oveq1d 6630 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)) = ( 1 · (𝐷𝐹)))
6534symgid 17761 . . . . . . . . . . . 12 (𝑁 ∈ Fin → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6632, 65syl 17 . . . . . . . . . . 11 (𝜑 → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
67663ad2ant1 1080 . . . . . . . . . 10 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
68673ad2ant1 1080 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6968fveq1d 6160 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
70 simp2 1060 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
71 fvresi 6404 . . . . . . . . 9 (𝑎𝑁 → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7270, 71syl 17 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7369, 72eqtr3d 2657 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ((0g‘(SymGrp‘𝑁))‘𝑎) = 𝑎)
7473oveq1d 6630 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏) = (𝑎𝐹𝑏))
7574mpt2eq3dva 6684 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
76 mdetuni.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
77 mdetuni.b . . . . . . . . 9 𝐵 = (Base‘𝐴)
7876, 52, 77matbas2i 20168 . . . . . . . 8 (𝐹𝐵𝐹 ∈ (𝐾𝑚 (𝑁 × 𝑁)))
79783ad2ant3 1082 . . . . . . 7 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 ∈ (𝐾𝑚 (𝑁 × 𝑁)))
80 elmapi 7839 . . . . . . 7 (𝐹 ∈ (𝐾𝑚 (𝑁 × 𝑁)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
81 ffn 6012 . . . . . . 7 (𝐹:(𝑁 × 𝑁)⟶𝐾𝐹 Fn (𝑁 × 𝑁))
8279, 80, 813syl 18 . . . . . 6 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 Fn (𝑁 × 𝑁))
83 fnov 6733 . . . . . 6 (𝐹 Fn (𝑁 × 𝑁) ↔ 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8482, 83sylib 208 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8575, 84eqtr4d 2658 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = 𝐹)
8685fveq2d 6162 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = (𝐷𝐹))
8756, 64, 863eqtr4rd 2666 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
88 simp2 1060 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑑 ∈ (Base‘(SymGrp‘𝑁)))
8939sseli 3584 . . . . . . . . . . . . 13 (𝑒 ∈ ran (pmTrsp‘𝑁) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
90893ad2ant3 1082 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
9134, 31, 30symgov 17750 . . . . . . . . . . . 12 ((𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9288, 90, 91syl2anc 692 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9392fveq1d 6160 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
94933ad2ant1 1080 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
9534, 31symgbasf1o 17743 . . . . . . . . . . . 12 (𝑒 ∈ (Base‘(SymGrp‘𝑁)) → 𝑒:𝑁1-1-onto𝑁)
96 f1of 6104 . . . . . . . . . . . 12 (𝑒:𝑁1-1-onto𝑁𝑒:𝑁𝑁)
9790, 95, 963syl 18 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒:𝑁𝑁)
98973ad2ant1 1080 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑒:𝑁𝑁)
99 simp2 1060 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
100 fvco3 6242 . . . . . . . . . 10 ((𝑒:𝑁𝑁𝑎𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10198, 99, 100syl2anc 692 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10294, 101eqtrd 2655 . . . . . . . 8 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
103102oveq1d 6630 . . . . . . 7 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏) = ((𝑑‘(𝑒𝑎))𝐹𝑏))
104103mpt2eq3dva 6684 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)))
105104fveq2d 6162 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))))
10634, 31symgbasf 17744 . . . . . 6 (𝑑 ∈ (Base‘(SymGrp‘𝑁)) → 𝑑:𝑁𝑁)
107 eqid 2621 . . . . . . . . 9 (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
108107, 38pmtrrn2 17820 . . . . . . . 8 (𝑒 ∈ ran (pmTrsp‘𝑁) → ∃𝑐𝑁𝑓𝑁 (𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})))
109 mdetuni.0g . . . . . . . . . . . . . 14 0 = (0g𝑅)
110 mdetuni.pg . . . . . . . . . . . . . 14 + = (+g𝑅)
111 mdetuni.al . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
112 mdetuni.li . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
113 mdetuni.sc . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
114 simpll1 1098 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝜑)
115 df-3an 1038 . . . . . . . . . . . . . . . 16 ((𝑐𝑁𝑓𝑁𝑐𝑓) ↔ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓))
116115biimpri 218 . . . . . . . . . . . . . . 15 (((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓) → (𝑐𝑁𝑓𝑁𝑐𝑓))
117116adantl 482 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑐𝑁𝑓𝑁𝑐𝑓))
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
119118adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
120119ad2antrr 761 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
121 simpllr 798 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑑:𝑁𝑁)
122 simprlr 802 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
123122adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑓𝑁)
124121, 123ffvelrnd 6326 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑓) ∈ 𝑁)
125 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑏𝑁)
126120, 124, 125fovrnd 6771 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑓)𝐹𝑏) ∈ 𝐾)
127 simprll 801 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
128127adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑐𝑁)
129121, 128ffvelrnd 6326 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑐) ∈ 𝑁)
130120, 129, 125fovrnd 6771 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑐)𝐹𝑏) ∈ 𝐾)
131126, 130jca 554 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (((𝑑𝑓)𝐹𝑏) ∈ 𝐾 ∧ ((𝑑𝑐)𝐹𝑏) ∈ 𝐾))
132118ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
1331323ad2ant1 1080 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
134 simp1lr 1123 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑑:𝑁𝑁)
135 simp2 1060 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
136134, 135ffvelrnd 6326 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → (𝑑𝑎) ∈ 𝑁)
137 simp3 1061 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
138133, 136, 137fovrnd 6771 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) ∈ 𝐾)
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 20363 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
140 simpl1 1062 . . . . . . . . . . . . . . 15 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝜑)
141 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑐 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐))
14232adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑁 ∈ Fin)
143 simprll 801 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
144 simprlr 802 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
145 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑓)
146107pmtrprfv 17813 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ Fin ∧ (𝑐𝑁𝑓𝑁𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
147142, 143, 144, 145, 146syl13anc 1325 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
148147adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
149141, 148sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑓)
150149fveq2d 6162 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑓))
151150oveq1d 6630 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
152 iftrue 4070 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
153152adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
154151, 153eqtr4d 2658 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
155 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑓 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓))
156 prcom 4244 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑐, 𝑓} = {𝑓, 𝑐}
157156fveq2i 6161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) = ((pmTrsp‘𝑁)‘{𝑓, 𝑐})
158157fveq1i 6159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓)
15932ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
160 simplrl 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑐𝑁𝑓𝑁))
161160simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑁)
162160simpld 475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑁)
163 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑓)
164163necomd 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑐)
165107pmtrprfv 17813 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ Fin ∧ (𝑓𝑁𝑐𝑁𝑓𝑐)) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
166159, 161, 162, 164, 165syl13anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
167158, 166syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = 𝑐)
168155, 167sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑐)
169168fveq2d 6162 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑐))
170169oveq1d 6630 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
171 iftrue 4070 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
172171adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
173170, 172eqtr4d 2658 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
174173adantlr 750 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
175 vex 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑎 ∈ V
176175elpr 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ {𝑐, 𝑓} ↔ (𝑎 = 𝑐𝑎 = 𝑓))
177176notbii 310 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ {𝑐, 𝑓} ↔ ¬ (𝑎 = 𝑐𝑎 = 𝑓))
178 ioran 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (𝑎 = 𝑐𝑎 = 𝑓) ↔ (¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓))
179177, 178sylbbr 226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
180179adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
181 prssi 4328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐𝑁𝑓𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
183 pr2ne 8788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐𝑁𝑓𝑁) → ({𝑐, 𝑓} ≈ 2𝑜𝑐𝑓))
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ({𝑐, 𝑓} ≈ 2𝑜𝑐𝑓))
185163, 184mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ≈ 2𝑜)
186107pmtrmvd 17816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2𝑜) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
187159, 182, 185, 186syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
188187eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ 𝑎 ∈ {𝑐, 𝑓}))
189188notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
190189ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
191180, 190mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ))
192107pmtrf 17815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2𝑜) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
193159, 182, 185, 192syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
194 ffn 6012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁 → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
195193, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
196 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑎𝑁)
197 fnelnfp 6408 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) ≠ 𝑎))
198197necon2bbid 2833 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
199195, 196, 198syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
200199ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
201191, 200mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎)
202201fveq2d 6162 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑎))
203202oveq1d 6630 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
204 iffalse 4073 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
205204adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
206203, 205eqtr4d 2658 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
207174, 206pm2.61dan 831 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
208 iffalse 4073 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
209208adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
210207, 209eqtr4d 2658 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
211154, 210pm2.61dan 831 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
2122113adant3 1079 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
213212mpt2eq3dva 6684 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
214140, 213sylan 488 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
215214fveq2d 6162 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
216 fveq2 6158 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑑𝑎) = (𝑑𝑐))
217216oveq1d 6630 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
218 iftrue 4070 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑐)𝐹𝑏))
219217, 218eqtr4d 2658 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
220 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑓 → (𝑑𝑎) = (𝑑𝑓))
221220oveq1d 6630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
222 iftrue 4070 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑓)𝐹𝑏))
223221, 222eqtr4d 2658 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
224223adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
225 iffalse 4073 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
226225eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
227226adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
228224, 227pm2.61dan 831 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
229 iffalse 4073 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
230228, 229eqtr4d 2658 . . . . . . . . . . . . . . . . . . 19 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
231219, 230pm2.61i 176 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
232231a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
233232mpt2eq3ia 6685 . . . . . . . . . . . . . . . 16 (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
234233fveq2i 6161 . . . . . . . . . . . . . . 15 (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
235234fveq2i 6161 . . . . . . . . . . . . . 14 ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
236235a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
237139, 215, 2363eqtr4d 2665 . . . . . . . . . . . 12 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
238 fveq1 6157 . . . . . . . . . . . . . . . . 17 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑒𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))
239238fveq2d 6162 . . . . . . . . . . . . . . . 16 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑑‘(𝑒𝑎)) = (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)))
240239oveq1d 6630 . . . . . . . . . . . . . . 15 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝑑‘(𝑒𝑎))𝐹𝑏) = ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))
241240mpt2eq3dv 6686 . . . . . . . . . . . . . 14 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)))
242241fveq2d 6162 . . . . . . . . . . . . 13 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))))
243242eqeq1d 2623 . . . . . . . . . . . 12 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
244237, 243syl5ibrcom 237 . . . . . . . . . . 11 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
245244expr 642 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → (𝑐𝑓 → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))))
246245impd 447 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → ((𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
247246rexlimdvva 3033 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (∃𝑐𝑁𝑓𝑁 (𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
248108, 247syl5 34 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (𝑒 ∈ ran (pmTrsp‘𝑁) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
2492483impia 1258 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
250106, 249syl3an2 1357 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
251105, 250eqtrd 2655 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
252251adantr 481 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
253 fveq2 6158 . . . 4 ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
254253adantl 482 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
255 eqid 2621 . . . . . 6 (invg𝑅) = (invg𝑅)
256473ad2ant1 1080 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑅 ∈ Ring)
257583ad2ant1 1080 . . . . . . . . 9 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2582573ad2ant1 1080 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
25959, 52mgpbas 18435 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
26031, 259mhmf 17280 . . . . . . . 8 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
261258, 260syl 17 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
262261, 88ffvelrnd 6326 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) ∈ 𝐾)
263493ad2ant1 1080 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐷:𝐵𝐾)
264 simp13 1091 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐹𝐵)
265263, 264ffvelrnd 6326 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷𝐹) ∈ 𝐾)
26652, 53, 255, 256, 262, 265ringmneg1 18536 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
26759, 53mgpplusg 18433 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
26831, 30, 267mhmlin 17282 . . . . . . . 8 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
269258, 88, 90, 268syl3anc 1323 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
270333ad2ant1 1080 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑁 ∈ Fin)
271 simp3 1061 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ran (pmTrsp‘𝑁))
27234, 31, 38pmtrodpm 19883 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
273270, 271, 272syl2anc 692 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
274 eqid 2621 . . . . . . . . . 10 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
275 eqid 2621 . . . . . . . . . 10 (pmSgn‘𝑁) = (pmSgn‘𝑁)
276274, 275, 54, 31, 255zrhpsgnodpm 19878 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
277256, 270, 273, 276syl3anc 1323 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
278277oveq2d 6631 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )))
27952, 53, 54, 255, 256, 262rngnegr 18535 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )) = ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)))
280269, 278, 2793eqtrrd 2660 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
281280oveq1d 6630 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
282266, 281eqtr3d 2657 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
283282adantr 481 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
284252, 254, 2833eqtrd 2659 . 2 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
285 simp2 1060 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸:𝑁1-1-onto𝑁)
28634, 31elsymgbas 17742 . . . 4 (𝑁 ∈ Fin → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
28733, 286syl 17 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
288285, 287mpbird 247 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸 ∈ (Base‘(SymGrp‘𝑁)))
2897, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 284, 288mrcmndind 17306 1 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2908  wrex 2909  cdif 3557  wss 3560  ifcif 4064  {csn 4155  {cpr 4157   class class class wbr 4623   I cid 4994   × cxp 5082  dom cdm 5084  ran crn 5085  cres 5086  ccom 5088   Fn wfn 5852  wf 5853  1-1-ontowf1o 5856  cfv 5857  (class class class)co 6615  cmpt2 6617  𝑓 cof 6860  2𝑜c2o 7514  𝑚 cmap 7817  cen 7912  Fincfn 7915  Basecbs 15800  +gcplusg 15881  .rcmulr 15882  0gc0g 16040  mrClscmrc 16183  Mndcmnd 17234   MndHom cmhm 17273  SubMndcsubmnd 17274  Grpcgrp 17362  invgcminusg 17363  SymGrpcsymg 17737  pmTrspcpmtr 17801  pmSgncpsgn 17849  pmEvencevpm 17850  mulGrpcmgp 18429  1rcur 18441  Ringcrg 18487  ℤRHomczrh 19788   Mat cmat 20153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-xor 1462  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-ot 4164  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-tpos 7312  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-sup 8308  df-card 8725  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-xnn0 11324  df-z 11338  df-dec 11454  df-uz 11648  df-rp 11793  df-fz 12285  df-fzo 12423  df-seq 12758  df-exp 12817  df-hash 13074  df-word 13254  df-lsw 13255  df-concat 13256  df-s1 13257  df-substr 13258  df-splice 13259  df-reverse 13260  df-s2 13546  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-0g 16042  df-gsum 16043  df-prds 16048  df-pws 16050  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-mhm 17275  df-submnd 17276  df-grp 17365  df-minusg 17366  df-mulg 17481  df-subg 17531  df-ghm 17598  df-gim 17641  df-oppg 17716  df-symg 17738  df-pmtr 17802  df-psgn 17851  df-evpm 17852  df-cmn 18135  df-abl 18136  df-mgp 18430  df-ur 18442  df-ring 18489  df-cring 18490  df-oppr 18563  df-dvdsr 18581  df-unit 18582  df-invr 18612  df-dvr 18623  df-rnghom 18655  df-drng 18689  df-subrg 18718  df-sra 19112  df-rgmod 19113  df-cnfld 19687  df-zring 19759  df-zrh 19792  df-dsmm 20016  df-frlm 20031  df-mat 20154
This theorem is referenced by:  mdetunilem8  20365
  Copyright terms: Public domain W3C validator