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

Theorem mdetunilem7 21221
Description: Lemma for mdetuni 21225. (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 6651 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
21oveq1d 7155 . . . . 5 (𝑐 = 𝑑 → ((𝑐𝑎)𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
32mpoeq3dv 7217 . . . 4 (𝑐 = 𝑑 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))
43fveq2d 6656 . . 3 (𝑐 = 𝑑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))
5 fveq2 6652 . . . 4 (𝑐 = 𝑑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑))
65oveq1d 7155 . . 3 (𝑐 = 𝑑 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)))
74, 6eqeq12d 2838 . 2 (𝑐 = 𝑑 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
8 fveq1 6651 . . . . . 6 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑐𝑎) = ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎))
98oveq1d 7155 . . . . 5 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝑐𝑎)𝐹𝑏) = (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))
109mpoeq3dv 7217 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)))
1110fveq2d 6656 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))))
12 fveq2 6652 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
1312oveq1d 7155 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
1411, 13eqeq12d 2838 . 2 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹))))
15 fveq1 6651 . . . . . 6 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑐𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
1615oveq1d 7155 . . . . 5 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝑐𝑎)𝐹𝑏) = (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))
1716mpoeq3dv 7217 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)))
1817fveq2d 6656 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))))
19 fveq2 6652 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))))
2019oveq1d 7155 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
2118, 20eqeq12d 2838 . 2 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹))))
22 fveq1 6651 . . . . . 6 (𝑐 = 𝐸 → (𝑐𝑎) = (𝐸𝑎))
2322oveq1d 7155 . . . . 5 (𝑐 = 𝐸 → ((𝑐𝑎)𝐹𝑏) = ((𝐸𝑎)𝐹𝑏))
2423mpoeq3dv 7217 . . . 4 (𝑐 = 𝐸 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏)))
2524fveq2d 6656 . . 3 (𝑐 = 𝐸 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))))
26 fveq2 6652 . . . 4 (𝑐 = 𝐸 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸))
2726oveq1d 7155 . . 3 (𝑐 = 𝐸 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
2825, 27eqeq12d 2838 . 2 (𝑐 = 𝐸 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹))))
29 eqid 2822 . 2 (0g‘(SymGrp‘𝑁)) = (0g‘(SymGrp‘𝑁))
30 eqid 2822 . 2 (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
31 eqid 2822 . 2 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
32 mdetuni.n . . . 4 (𝜑𝑁 ∈ Fin)
33323ad2ant1 1130 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑁 ∈ Fin)
34 eqid 2822 . . . 4 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3534symggrp 18519 . . 3 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
36 grpmnd 18101 . . 3 ((SymGrp‘𝑁) ∈ Grp → (SymGrp‘𝑁) ∈ Mnd)
3733, 35, 363syl 18 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (SymGrp‘𝑁) ∈ Mnd)
38 eqid 2822 . . . 4 ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
3938, 34, 31symgtrf 18588 . . 3 ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
4039a1i 11 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
41 eqid 2822 . . . . . 6 (mrCls‘(SubMnd‘(SymGrp‘𝑁))) = (mrCls‘(SubMnd‘(SymGrp‘𝑁)))
4238, 34, 31, 41symggen2 18590 . . . . 5 (𝑁 ∈ Fin → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4332, 42syl 17 . . . 4 (𝜑 → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4443eqcomd 2828 . . 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, 50ffvelrnd 6834 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷𝐹) ∈ 𝐾)
52 mdetuni.k . . . . 5 𝐾 = (Base‘𝑅)
53 mdetuni.tg . . . . 5 · = (.r𝑅)
54 mdetuni.1r . . . . 5 1 = (1r𝑅)
5552, 53, 54ringlidm 19315 . . . 4 ((𝑅 ∈ Ring ∧ (𝐷𝐹) ∈ 𝐾) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
5647, 51, 55syl2anc 587 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
57 zrhpsgnmhm 20271 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
5846, 32, 57syl2anc 587 . . . . . 6 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
59 eqid 2822 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
6059, 54ringidval 19244 . . . . . . 7 1 = (0g‘(mulGrp‘𝑅))
6129, 60mhm0 17955 . . . . . 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 7155 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)) = ( 1 · (𝐷𝐹)))
6534symgid 18520 . . . . . . . . . . . 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 6654 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
70 simp2 1134 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
71 fvresi 6917 . . . . . . . . 9 (𝑎𝑁 → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7270, 71syl 17 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7369, 72eqtr3d 2859 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ((0g‘(SymGrp‘𝑁))‘𝑎) = 𝑎)
7473oveq1d 7155 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏) = (𝑎𝐹𝑏))
7574mpoeq3dva 7215 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
76 mdetuni.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
77 mdetuni.b . . . . . . . . 9 𝐵 = (Base‘𝐴)
7876, 52, 77matbas2i 21025 . . . . . . . 8 (𝐹𝐵𝐹 ∈ (𝐾m (𝑁 × 𝑁)))
79783ad2ant3 1132 . . . . . . 7 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 ∈ (𝐾m (𝑁 × 𝑁)))
80 elmapi 8415 . . . . . . 7 (𝐹 ∈ (𝐾m (𝑁 × 𝑁)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
81 ffn 6494 . . . . . . 7 (𝐹:(𝑁 × 𝑁)⟶𝐾𝐹 Fn (𝑁 × 𝑁))
8279, 80, 813syl 18 . . . . . 6 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 Fn (𝑁 × 𝑁))
83 fnov 7266 . . . . . 6 (𝐹 Fn (𝑁 × 𝑁) ↔ 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8482, 83sylib 221 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8575, 84eqtr4d 2860 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = 𝐹)
8685fveq2d 6656 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = (𝐷𝐹))
8756, 64, 863eqtr4rd 2868 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
88 simp2 1134 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑑 ∈ (Base‘(SymGrp‘𝑁)))
8939sseli 3938 . . . . . . . . . . . . 13 (𝑒 ∈ ran (pmTrsp‘𝑁) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
90893ad2ant3 1132 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
9134, 31, 30symgov 18503 . . . . . . . . . . . 12 ((𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9288, 90, 91syl2anc 587 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9392fveq1d 6654 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
94933ad2ant1 1130 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
9534, 31symgbasf1o 18494 . . . . . . . . . . . 12 (𝑒 ∈ (Base‘(SymGrp‘𝑁)) → 𝑒:𝑁1-1-onto𝑁)
96 f1of 6597 . . . . . . . . . . . 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 6742 . . . . . . . . . 10 ((𝑒:𝑁𝑁𝑎𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10198, 99, 100syl2anc 587 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10294, 101eqtrd 2857 . . . . . . . 8 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
103102oveq1d 7155 . . . . . . 7 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏) = ((𝑑‘(𝑒𝑎))𝐹𝑏))
104103mpoeq3dva 7215 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)))
105104fveq2d 6656 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))))
10634, 31symgbasf 18495 . . . . . 6 (𝑑 ∈ (Base‘(SymGrp‘𝑁)) → 𝑑:𝑁𝑁)
107 eqid 2822 . . . . . . . . 9 (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
108107, 38pmtrrn2 18579 . . . . . . . 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 231 . . . . . . . . . . . . . . 15 (((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓) → (𝑐𝑁𝑓𝑁𝑐𝑓))
117116adantl 485 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑐𝑁𝑓𝑁𝑐𝑓))
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
119118adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
120119ad2antrr 725 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
121 simpllr 775 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑑:𝑁𝑁)
122 simprlr 779 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
123122adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑓𝑁)
124121, 123ffvelrnd 6834 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑓) ∈ 𝑁)
125 simpr 488 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑏𝑁)
126120, 124, 125fovrnd 7305 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑓)𝐹𝑏) ∈ 𝐾)
127 simprll 778 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
128127adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑐𝑁)
129121, 128ffvelrnd 6834 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑐) ∈ 𝑁)
130120, 129, 125fovrnd 7305 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑐)𝐹𝑏) ∈ 𝐾)
131126, 130jca 515 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (((𝑑𝑓)𝐹𝑏) ∈ 𝐾 ∧ ((𝑑𝑐)𝐹𝑏) ∈ 𝐾))
132118ad2antrr 725 . . . . . . . . . . . . . . . 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, 135ffvelrnd 6834 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → (𝑑𝑎) ∈ 𝑁)
137 simp3 1135 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
138133, 136, 137fovrnd 7305 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) ∈ 𝐾)
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 21220 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
140 simpl1 1188 . . . . . . . . . . . . . . 15 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝜑)
141 fveq2 6652 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑐 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐))
14232adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑁 ∈ Fin)
143 simprll 778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
144 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
145 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑓)
146107pmtrprfv 18572 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ Fin ∧ (𝑐𝑁𝑓𝑁𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
147142, 143, 144, 145, 146syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
148147adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
149141, 148sylan9eqr 2879 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑓)
150149fveq2d 6656 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑓))
151150oveq1d 7155 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
152 iftrue 4445 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
153152adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
154151, 153eqtr4d 2860 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
155 fveq2 6652 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑓 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓))
156 prcom 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑐, 𝑓} = {𝑓, 𝑐}
157156fveq2i 6655 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) = ((pmTrsp‘𝑁)‘{𝑓, 𝑐})
158157fveq1i 6653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓)
15932ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
160 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑐𝑁𝑓𝑁))
161160simprd 499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑁)
162160simpld 498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑁)
163 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑓)
164163necomd 3066 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑐)
165107pmtrprfv 18572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ Fin ∧ (𝑓𝑁𝑐𝑁𝑓𝑐)) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
166159, 161, 162, 164, 165syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
167158, 166syl5eq 2869 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = 𝑐)
168155, 167sylan9eqr 2879 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑐)
169168fveq2d 6656 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑐))
170169oveq1d 7155 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
171 iftrue 4445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
172171adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
173170, 172eqtr4d 2860 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
174173adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
175 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑎 ∈ V
176175elpr 4562 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ {𝑐, 𝑓} ↔ (𝑎 = 𝑐𝑎 = 𝑓))
177176notbii 323 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ {𝑐, 𝑓} ↔ ¬ (𝑎 = 𝑐𝑎 = 𝑓))
178 ioran 981 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (𝑎 = 𝑐𝑎 = 𝑓) ↔ (¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓))
179177, 178sylbbr 239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
180179adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
181 prssi 4727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐𝑁𝑓𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
183 pr2ne 9420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐𝑁𝑓𝑁) → ({𝑐, 𝑓} ≈ 2o𝑐𝑓))
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ({𝑐, 𝑓} ≈ 2o𝑐𝑓))
185163, 184mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ≈ 2o)
186107pmtrmvd 18575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2o) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
187159, 182, 185, 186syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
188187eleq2d 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ 𝑎 ∈ {𝑐, 𝑓}))
189188notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
190189ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
191180, 190mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ))
192107pmtrf 18574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2o) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
193159, 182, 185, 192syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
194193ffnd 6495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
195 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑎𝑁)
196 fnelnfp 6921 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) ≠ 𝑎))
197196necon2bbid 3054 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
198194, 195, 197syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
199198ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
200191, 199mpbird 260 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎)
201200fveq2d 6656 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑎))
202201oveq1d 7155 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
203 iffalse 4448 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
204203adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
205202, 204eqtr4d 2860 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
206174, 205pm2.61dan 812 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
207 iffalse 4448 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
208207adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
209206, 208eqtr4d 2860 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
210154, 209pm2.61dan 812 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
2112103adant3 1129 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
212211mpoeq3dva 7215 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
213140, 212sylan 583 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
214213fveq2d 6656 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
215 fveq2 6652 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑑𝑎) = (𝑑𝑐))
216215oveq1d 7155 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
217 iftrue 4445 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑐)𝐹𝑏))
218216, 217eqtr4d 2860 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
219 fveq2 6652 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑓 → (𝑑𝑎) = (𝑑𝑓))
220219oveq1d 7155 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
221 iftrue 4445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑓)𝐹𝑏))
222220, 221eqtr4d 2860 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
223222adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
224 iffalse 4448 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
225224eqcomd 2828 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
226225adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
227223, 226pm2.61dan 812 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
228 iffalse 4448 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
229227, 228eqtr4d 2860 . . . . . . . . . . . . . . . . . . 19 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
230218, 229pm2.61i 185 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
231230a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
232231mpoeq3ia 7216 . . . . . . . . . . . . . . . 16 (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
233232fveq2i 6655 . . . . . . . . . . . . . . 15 (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
234233fveq2i 6655 . . . . . . . . . . . . . 14 ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
235234a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
236139, 214, 2353eqtr4d 2867 . . . . . . . . . . . 12 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
237 fveq1 6651 . . . . . . . . . . . . . . . 16 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑒𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))
238237fveq2d 6656 . . . . . . . . . . . . . . 15 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑑‘(𝑒𝑎)) = (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)))
239238oveq1d 7155 . . . . . . . . . . . . . 14 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝑑‘(𝑒𝑎))𝐹𝑏) = ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))
240239mpoeq3dv 7217 . . . . . . . . . . . . 13 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)))
241240fveqeq2d 6660 . . . . . . . . . . . 12 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
242236, 241syl5ibrcom 250 . . . . . . . . . . 11 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
243242expr 460 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → (𝑐𝑓 → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))))
244243impd 414 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → ((𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
245244rexlimdvva 3280 . . . . . . . 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 2857 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
250249adantr 484 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
251 fveq2 6652 . . . 4 ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
252251adantl 485 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
253 eqid 2822 . . . . . 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 19236 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
25831, 257mhmf 17952 . . . . . . . 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, 88ffvelrnd 6834 . . . . . 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, 262ffvelrnd 6834 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷𝐹) ∈ 𝐾)
26452, 53, 253, 254, 260, 263ringmneg1 19340 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
26559, 53mgpplusg 19234 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
26631, 30, 265mhmlin 17954 . . . . . . . 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 20284 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
271268, 269, 270syl2anc 587 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
272 eqid 2822 . . . . . . . . . 10 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
273 eqid 2822 . . . . . . . . . 10 (pmSgn‘𝑁) = (pmSgn‘𝑁)
274272, 273, 54, 31, 253zrhpsgnodpm 20279 . . . . . . . . 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 7156 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )))
27752, 53, 54, 253, 254, 260rngnegr 19339 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )) = ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)))
278267, 276, 2773eqtrrd 2862 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
279278oveq1d 7155 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
280264, 279eqtr3d 2859 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
281280adantr 484 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
282250, 252, 2813eqtrd 2861 . 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 18493 . . . 4 (𝑁 ∈ Fin → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
28533, 284syl 17 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁1-1-onto𝑁))
286283, 285mpbird 260 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸 ∈ (Base‘(SymGrp‘𝑁)))
2877, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 282, 286mndind 17983 1 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2114  wne 3011  wral 3130  wrex 3131  cdif 3905  wss 3908  ifcif 4439  {csn 4539  {cpr 4541   class class class wbr 5042   I cid 5436   × cxp 5530  dom cdm 5532  ran crn 5533  cres 5534  ccom 5536   Fn wfn 6329  wf 6330  1-1-ontowf1o 6333  cfv 6334  (class class class)co 7140  cmpo 7142  f cof 7392  2oc2o 8083  m cmap 8393  cen 8493  Fincfn 8496  Basecbs 16474  +gcplusg 16556  .rcmulr 16557  0gc0g 16704  mrClscmrc 16845  Mndcmnd 17902   MndHom cmhm 17945  SubMndcsubmnd 17946  Grpcgrp 18094  invgcminusg 18095  SymGrpcsymg 18486  pmTrspcpmtr 18560  pmSgncpsgn 18608  pmEvencevpm 18609  mulGrpcmgp 19230  1rcur 19242  Ringcrg 19288  ℤRHomczrh 20191   Mat cmat 21010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-xor 1503  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-ot 4548  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-xnn0 11956  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-fz 12886  df-fzo 13029  df-seq 13365  df-exp 13426  df-hash 13687  df-word 13858  df-lsw 13906  df-concat 13914  df-s1 13941  df-substr 13994  df-pfx 14024  df-splice 14103  df-reverse 14112  df-s2 14201  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-mulr 16570  df-starv 16571  df-sca 16572  df-vsca 16573  df-ip 16574  df-tset 16575  df-ple 16576  df-ds 16578  df-unif 16579  df-hom 16580  df-cco 16581  df-0g 16706  df-gsum 16707  df-prds 16712  df-pws 16714  df-mre 16848  df-mrc 16849  df-acs 16851  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-mhm 17947  df-submnd 17948  df-efmnd 18025  df-grp 18097  df-minusg 18098  df-mulg 18216  df-subg 18267  df-ghm 18347  df-gim 18390  df-oppg 18465  df-symg 18487  df-pmtr 18561  df-psgn 18610  df-evpm 18611  df-cmn 18899  df-abl 18900  df-mgp 19231  df-ur 19243  df-ring 19290  df-cring 19291  df-oppr 19367  df-dvdsr 19385  df-unit 19386  df-invr 19416  df-dvr 19427  df-rnghom 19461  df-drng 19495  df-subrg 19524  df-sra 19935  df-rgmod 19936  df-cnfld 20090  df-zring 20162  df-zrh 20195  df-dsmm 20419  df-frlm 20434  df-mat 21011
This theorem is referenced by:  mdetunilem8  21222
  Copyright terms: Public domain W3C validator