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

Theorem mdetunilem7 20626
Description: Lemma for mdetuni 20630. (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 6351 . . . . . 6 (𝑐 = 𝑑 → (𝑐𝑎) = (𝑑𝑎))
21oveq1d 6828 . . . . 5 (𝑐 = 𝑑 → ((𝑐𝑎)𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
32mpt2eq3dv 6886 . . . 4 (𝑐 = 𝑑 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))
43fveq2d 6356 . . 3 (𝑐 = 𝑑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))
5 fveq2 6352 . . . 4 (𝑐 = 𝑑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑))
65oveq1d 6828 . . 3 (𝑐 = 𝑑 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)))
74, 6eqeq12d 2775 . 2 (𝑐 = 𝑑 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
8 fveq1 6351 . . . . . 6 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑐𝑎) = ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎))
98oveq1d 6828 . . . . 5 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝑐𝑎)𝐹𝑏) = (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))
109mpt2eq3dv 6886 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)))
1110fveq2d 6356 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))))
12 fveq2 6352 . . . 4 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
1312oveq1d 6828 . . 3 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
1411, 13eqeq12d 2775 . 2 (𝑐 = (𝑑(+g‘(SymGrp‘𝑁))𝑒) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹))))
15 fveq1 6351 . . . . . 6 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑐𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
1615oveq1d 6828 . . . . 5 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝑐𝑎)𝐹𝑏) = (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))
1716mpt2eq3dv 6886 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)))
1817fveq2d 6356 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))))
19 fveq2 6352 . . . 4 (𝑐 = (0g‘(SymGrp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))))
2019oveq1d 6828 . . 3 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
2118, 20eqeq12d 2775 . 2 (𝑐 = (0g‘(SymGrp‘𝑁)) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹))))
22 fveq1 6351 . . . . . 6 (𝑐 = 𝐸 → (𝑐𝑎) = (𝐸𝑎))
2322oveq1d 6828 . . . . 5 (𝑐 = 𝐸 → ((𝑐𝑎)𝐹𝑏) = ((𝐸𝑎)𝐹𝑏))
2423mpt2eq3dv 6886 . . . 4 (𝑐 = 𝐸 → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏)))
2524fveq2d 6356 . . 3 (𝑐 = 𝐸 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))))
26 fveq2 6352 . . . 4 (𝑐 = 𝐸 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸))
2726oveq1d 6828 . . 3 (𝑐 = 𝐸 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
2825, 27eqeq12d 2775 . 2 (𝑐 = 𝐸 → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑐𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷𝐹)) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹))))
29 eqid 2760 . 2 (0g‘(SymGrp‘𝑁)) = (0g‘(SymGrp‘𝑁))
30 eqid 2760 . 2 (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
31 eqid 2760 . 2 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
32 mdetuni.n . . . 4 (𝜑𝑁 ∈ Fin)
33323ad2ant1 1128 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑁 ∈ Fin)
34 eqid 2760 . . . 4 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3534symggrp 18020 . . 3 (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
36 grpmnd 17630 . . 3 ((SymGrp‘𝑁) ∈ Grp → (SymGrp‘𝑁) ∈ Mnd)
3733, 35, 363syl 18 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (SymGrp‘𝑁) ∈ Mnd)
38 eqid 2760 . . . 4 ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
3938, 34, 31symgtrf 18089 . . 3 ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
4039a1i 11 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
41 eqid 2760 . . . . . 6 (mrCls‘(SubMnd‘(SymGrp‘𝑁))) = (mrCls‘(SubMnd‘(SymGrp‘𝑁)))
4238, 34, 31, 41symggen2 18091 . . . . 5 (𝑁 ∈ Fin → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4332, 42syl 17 . . . 4 (𝜑 → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
4443eqcomd 2766 . . 3 (𝜑 → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
45443ad2ant1 1128 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
46 mdetuni.r . . . . 5 (𝜑𝑅 ∈ Ring)
47463ad2ant1 1128 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝑅 ∈ Ring)
48 mdetuni.ff . . . . . 6 (𝜑𝐷:𝐵𝐾)
49483ad2ant1 1128 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐷:𝐵𝐾)
50 simp3 1133 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹𝐵)
5149, 50ffvelrnd 6523 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷𝐹) ∈ 𝐾)
52 mdetuni.k . . . . 5 𝐾 = (Base‘𝑅)
53 mdetuni.tg . . . . 5 · = (.r𝑅)
54 mdetuni.1r . . . . 5 1 = (1r𝑅)
5552, 53, 54ringlidm 18771 . . . 4 ((𝑅 ∈ Ring ∧ (𝐷𝐹) ∈ 𝐾) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
5647, 51, 55syl2anc 696 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( 1 · (𝐷𝐹)) = (𝐷𝐹))
57 zrhpsgnmhm 20132 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
5846, 32, 57syl2anc 696 . . . . . 6 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
59 eqid 2760 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
6059, 54ringidval 18703 . . . . . . 7 1 = (0g‘(mulGrp‘𝑅))
6129, 60mhm0 17544 . . . . . 6 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6258, 61syl 17 . . . . 5 (𝜑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
63623ad2ant1 1128 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) = 1 )
6463oveq1d 6828 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)) = ( 1 · (𝐷𝐹)))
6534symgid 18021 . . . . . . . . . . . 12 (𝑁 ∈ Fin → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6632, 65syl 17 . . . . . . . . . . 11 (𝜑 → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
67663ad2ant1 1128 . . . . . . . . . 10 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
68673ad2ant1 1128 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ( I ↾ 𝑁) = (0g‘(SymGrp‘𝑁)))
6968fveq1d 6354 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = ((0g‘(SymGrp‘𝑁))‘𝑎))
70 simp2 1132 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
71 fvresi 6603 . . . . . . . . 9 (𝑎𝑁 → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7270, 71syl 17 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (( I ↾ 𝑁)‘𝑎) = 𝑎)
7369, 72eqtr3d 2796 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → ((0g‘(SymGrp‘𝑁))‘𝑎) = 𝑎)
7473oveq1d 6828 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑎𝑁𝑏𝑁) → (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏) = (𝑎𝐹𝑏))
7574mpt2eq3dva 6884 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
76 mdetuni.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
77 mdetuni.b . . . . . . . . 9 𝐵 = (Base‘𝐴)
7876, 52, 77matbas2i 20430 . . . . . . . 8 (𝐹𝐵𝐹 ∈ (𝐾𝑚 (𝑁 × 𝑁)))
79783ad2ant3 1130 . . . . . . 7 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 ∈ (𝐾𝑚 (𝑁 × 𝑁)))
80 elmapi 8045 . . . . . . 7 (𝐹 ∈ (𝐾𝑚 (𝑁 × 𝑁)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
81 ffn 6206 . . . . . . 7 (𝐹:(𝑁 × 𝑁)⟶𝐾𝐹 Fn (𝑁 × 𝑁))
8279, 80, 813syl 18 . . . . . 6 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 Fn (𝑁 × 𝑁))
83 fnov 6933 . . . . . 6 (𝐹 Fn (𝑁 × 𝑁) ↔ 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8482, 83sylib 208 . . . . 5 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹 = (𝑎𝑁, 𝑏𝑁 ↦ (𝑎𝐹𝑏)))
8575, 84eqtr4d 2797 . . . 4 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = 𝐹)
8685fveq2d 6356 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = (𝐷𝐹))
8756, 64, 863eqtr4rd 2805 . 2 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((0g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0g‘(SymGrp‘𝑁))) · (𝐷𝐹)))
88 simp2 1132 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑑 ∈ (Base‘(SymGrp‘𝑁)))
8939sseli 3740 . . . . . . . . . . . . 13 (𝑒 ∈ ran (pmTrsp‘𝑁) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
90893ad2ant3 1130 . . . . . . . . . . . 12 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
9134, 31, 30symgov 18010 . . . . . . . . . . . 12 ((𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9288, 90, 91syl2anc 696 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑑(+g‘(SymGrp‘𝑁))𝑒) = (𝑑𝑒))
9392fveq1d 6354 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
94933ad2ant1 1128 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑𝑒)‘𝑎))
9534, 31symgbasf1o 18003 . . . . . . . . . . . 12 (𝑒 ∈ (Base‘(SymGrp‘𝑁)) → 𝑒:𝑁1-1-onto𝑁)
96 f1of 6298 . . . . . . . . . . . 12 (𝑒:𝑁1-1-onto𝑁𝑒:𝑁𝑁)
9790, 95, 963syl 18 . . . . . . . . . . 11 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒:𝑁𝑁)
98973ad2ant1 1128 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑒:𝑁𝑁)
99 simp2 1132 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
100 fvco3 6437 . . . . . . . . . 10 ((𝑒:𝑁𝑁𝑎𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10198, 99, 100syl2anc 696 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
10294, 101eqtrd 2794 . . . . . . . 8 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎) = (𝑑‘(𝑒𝑎)))
103102oveq1d 6828 . . . . . . 7 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎𝑁𝑏𝑁) → (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏) = ((𝑑‘(𝑒𝑎))𝐹𝑏))
104103mpt2eq3dva 6884 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)))
105104fveq2d 6356 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))))
10634, 31symgbasf 18004 . . . . . 6 (𝑑 ∈ (Base‘(SymGrp‘𝑁)) → 𝑑:𝑁𝑁)
107 eqid 2760 . . . . . . . . 9 (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
108107, 38pmtrrn2 18080 . . . . . . . 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 1255 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝜑)
115 df-3an 1074 . . . . . . . . . . . . . . . 16 ((𝑐𝑁𝑓𝑁𝑐𝑓) ↔ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓))
116115biimpri 218 . . . . . . . . . . . . . . 15 (((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓) → (𝑐𝑁𝑓𝑁𝑐𝑓))
117116adantl 473 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑐𝑁𝑓𝑁𝑐𝑓))
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
119118adantr 472 . . . . . . . . . . . . . . . . 17 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
120119ad2antrr 764 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
121 simpllr 817 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑑:𝑁𝑁)
122 simprlr 822 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
123122adantr 472 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑓𝑁)
124121, 123ffvelrnd 6523 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑓) ∈ 𝑁)
125 simpr 479 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑏𝑁)
126120, 124, 125fovrnd 6971 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑓)𝐹𝑏) ∈ 𝐾)
127 simprll 821 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
128127adantr 472 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → 𝑐𝑁)
129121, 128ffvelrnd 6523 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (𝑑𝑐) ∈ 𝑁)
130120, 129, 125fovrnd 6971 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → ((𝑑𝑐)𝐹𝑏) ∈ 𝐾)
131126, 130jca 555 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑏𝑁) → (((𝑑𝑓)𝐹𝑏) ∈ 𝐾 ∧ ((𝑑𝑐)𝐹𝑏) ∈ 𝐾))
132118ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
1331323ad2ant1 1128 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
134 simp1lr 1304 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑑:𝑁𝑁)
135 simp2 1132 . . . . . . . . . . . . . . . 16 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑎𝑁)
136134, 135ffvelrnd 6523 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → (𝑑𝑎) ∈ 𝑁)
137 simp3 1133 . . . . . . . . . . . . . . 15 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
138133, 136, 137fovrnd 6971 . . . . . . . . . . . . . 14 (((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) ∈ 𝐾)
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 20625 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
140 simpl1 1228 . . . . . . . . . . . . . . 15 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → 𝜑)
141 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑐 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐))
14232adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑁 ∈ Fin)
143 simprll 821 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑁)
144 simprlr 822 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑓𝑁)
145 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → 𝑐𝑓)
146107pmtrprfv 18073 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ Fin ∧ (𝑐𝑁𝑓𝑁𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
147142, 143, 144, 145, 146syl13anc 1479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
148147adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
149141, 148sylan9eqr 2816 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑓)
150149fveq2d 6356 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑓))
151150oveq1d 6828 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
152 iftrue 4236 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
153152adantl 473 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑓)𝐹𝑏))
154151, 153eqtr4d 2797 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
155 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑓 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓))
156 prcom 4411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑐, 𝑓} = {𝑓, 𝑐}
157156fveq2i 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) = ((pmTrsp‘𝑁)‘{𝑓, 𝑐})
158157fveq1i 6353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓)
15932ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
160 simplrl 819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑐𝑁𝑓𝑁))
161160simprd 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑁)
162160simpld 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑁)
163 simplrr 820 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑐𝑓)
164163necomd 2987 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑓𝑐)
165107pmtrprfv 18073 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ Fin ∧ (𝑓𝑁𝑐𝑁𝑓𝑐)) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
166159, 161, 162, 164, 165syl13anc 1479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
167158, 166syl5eq 2806 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = 𝑐)
168155, 167sylan9eqr 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑐)
169168fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑐))
170169oveq1d 6828 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
171 iftrue 4236 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
172171adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑐)𝐹𝑏))
173170, 172eqtr4d 2797 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
174173adantlr 753 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
175 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑎 ∈ V
176175elpr 4343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ {𝑐, 𝑓} ↔ (𝑎 = 𝑐𝑎 = 𝑓))
177176notbii 309 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ {𝑐, 𝑓} ↔ ¬ (𝑎 = 𝑐𝑎 = 𝑓))
178 ioran 512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (𝑎 = 𝑐𝑎 = 𝑓) ↔ (¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓))
179177, 178sylbbr 226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
180179adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
181 prssi 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐𝑁𝑓𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
183 pr2ne 9018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐𝑁𝑓𝑁) → ({𝑐, 𝑓} ≈ 2𝑜𝑐𝑓))
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ({𝑐, 𝑓} ≈ 2𝑜𝑐𝑓))
185163, 184mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → {𝑐, 𝑓} ≈ 2𝑜)
186107pmtrmvd 18076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2𝑜) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
187159, 182, 185, 186syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
188187eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ 𝑎 ∈ {𝑐, 𝑓}))
189188notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
190189ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
191180, 190mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ))
192107pmtrf 18075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2𝑜) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
193159, 182, 185, 192syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁)
194 ffn 6206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁𝑁 → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
195193, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
196 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → 𝑎𝑁)
197 fnelnfp 6607 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) ≠ 𝑎))
198197necon2bbid 2975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
199195, 196, 198syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
200199ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
201191, 200mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎)
202201fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑𝑎))
203202oveq1d 6828 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑𝑎)𝐹𝑏))
204 iffalse 4239 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
205204adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
206203, 205eqtr4d 2797 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
207174, 206pm2.61dan 867 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
208 iffalse 4239 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
209208adantl 473 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
210207, 209eqtr4d 2797 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
211154, 210pm2.61dan 867 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
2122113adant3 1127 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) ∧ 𝑎𝑁𝑏𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
213212mpt2eq3dva 6884 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
214140, 213sylan 489 . . . . . . . . . . . . . 14 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
215214fveq2d 6356 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑐)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
216 fveq2 6352 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑑𝑎) = (𝑑𝑐))
217216oveq1d 6828 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑐)𝐹𝑏))
218 iftrue 4236 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = ((𝑑𝑐)𝐹𝑏))
219217, 218eqtr4d 2797 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
220 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑓 → (𝑑𝑎) = (𝑑𝑓))
221220oveq1d 6828 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = ((𝑑𝑓)𝐹𝑏))
222 iftrue 4236 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑓)𝐹𝑏))
223221, 222eqtr4d 2797 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
224223adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
225 iffalse 4239 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)) = ((𝑑𝑎)𝐹𝑏))
226225eqcomd 2766 . . . . . . . . . . . . . . . . . . . . . 22 𝑎 = 𝑓 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
227226adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
228224, 227pm2.61dan 867 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
229 iffalse 4239 . . . . . . . . . . . . . . . . . . . 20 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
230228, 229eqtr4d 2797 . . . . . . . . . . . . . . . . . . 19 𝑎 = 𝑐 → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
231219, 230pm2.61i 176 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))
232231a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑎𝑁𝑏𝑁) → ((𝑑𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
233232mpt2eq3ia 6885 . . . . . . . . . . . . . . . 16 (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))
234233fveq2i 6355 . . . . . . . . . . . . . . 15 (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))
235234fveq2i 6355 . . . . . . . . . . . . . 14 ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏))))))
236235a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑐, ((𝑑𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑𝑓)𝐹𝑏), ((𝑑𝑎)𝐹𝑏)))))))
237139, 215, 2363eqtr4d 2804 . . . . . . . . . . . 12 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
238 fveq1 6351 . . . . . . . . . . . . . . . . 17 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑒𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))
239238fveq2d 6356 . . . . . . . . . . . . . . . 16 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑑‘(𝑒𝑎)) = (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)))
240239oveq1d 6828 . . . . . . . . . . . . . . 15 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝑑‘(𝑒𝑎))𝐹𝑏) = ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))
241240mpt2eq3dv 6886 . . . . . . . . . . . . . 14 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏)) = (𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)))
242241fveq2d 6356 . . . . . . . . . . . . 13 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))))
243242eqeq1d 2762 . . . . . . . . . . . 12 (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) ↔ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
244237, 243syl5ibrcom 237 . . . . . . . . . . 11 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ ((𝑐𝑁𝑓𝑁) ∧ 𝑐𝑓)) → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
245244expr 644 . . . . . . . . . 10 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → (𝑐𝑓 → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))))
246245impd 446 . . . . . . . . 9 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) ∧ (𝑐𝑁𝑓𝑁)) → ((𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
247246rexlimdvva 3176 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (∃𝑐𝑁𝑓𝑁 (𝑐𝑓𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
248108, 247syl5 34 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁) → (𝑒 ∈ ran (pmTrsp‘𝑁) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))))))
2492483impia 1110 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑:𝑁𝑁𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
250106, 249syl3an2 1168 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑‘(𝑒𝑎))𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
251105, 250eqtrd 2794 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
252251adantr 472 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))))
253 fveq2 6352 . . . 4 ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹)) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
254253adantl 473 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏)))) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
255 eqid 2760 . . . . . 6 (invg𝑅) = (invg𝑅)
256473ad2ant1 1128 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑅 ∈ Ring)
257583ad2ant1 1128 . . . . . . . . 9 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2582573ad2ant1 1128 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
25959, 52mgpbas 18695 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
26031, 259mhmf 17541 . . . . . . . 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 6523 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) ∈ 𝐾)
263493ad2ant1 1128 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐷:𝐵𝐾)
264 simp13 1248 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐹𝐵)
265263, 264ffvelrnd 6523 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷𝐹) ∈ 𝐾)
26652, 53, 255, 256, 262, 265ringmneg1 18796 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))))
26759, 53mgpplusg 18693 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
26831, 30, 267mhmlin 17543 . . . . . . . 8 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
269258, 88, 90, 268syl3anc 1477 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
270333ad2ant1 1128 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑁 ∈ Fin)
271 simp3 1133 . . . . . . . . . 10 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ran (pmTrsp‘𝑁))
27234, 31, 38pmtrodpm 20145 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
273270, 271, 272syl2anc 696 . . . . . . . . 9 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
274 eqid 2760 . . . . . . . . . 10 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
275 eqid 2760 . . . . . . . . . 10 (pmSgn‘𝑁) = (pmSgn‘𝑁)
276274, 275, 54, 31, 255zrhpsgnodpm 20140 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
277256, 270, 273, 276syl3anc 1477 . . . . . . . 8 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((invg𝑅)‘ 1 ))
278277oveq2d 6829 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )))
27952, 53, 54, 255, 256, 262rngnegr 18795 . . . . . . 7 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((invg𝑅)‘ 1 )) = ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)))
280269, 278, 2793eqtrrd 2799 . . . . . 6 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)))
281280oveq1d 6828 . . . . 5 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((invg𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
282266, 281eqtr3d 2796 . . . 4 (((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
283282adantr 472 . . 3 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → ((invg𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
284252, 254, 2833eqtrd 2798 . 2 ((((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝑑𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷𝐹))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ (((𝑑(+g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+g‘(SymGrp‘𝑁))𝑒)) · (𝐷𝐹)))
285 simp2 1132 . . 3 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → 𝐸:𝑁1-1-onto𝑁)
28634, 31elsymgbas 18002 . . . 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 17567 1 ((𝜑𝐸:𝑁1-1-onto𝑁𝐹𝐵) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ ((𝐸𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  cdif 3712  wss 3715  ifcif 4230  {csn 4321  {cpr 4323   class class class wbr 4804   I cid 5173   × cxp 5264  dom cdm 5266  ran crn 5267  cres 5268  ccom 5270   Fn wfn 6044  wf 6045  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  cmpt2 6815  𝑓 cof 7060  2𝑜c2o 7723  𝑚 cmap 8023  cen 8118  Fincfn 8121  Basecbs 16059  +gcplusg 16143  .rcmulr 16144  0gc0g 16302  mrClscmrc 16445  Mndcmnd 17495   MndHom cmhm 17534  SubMndcsubmnd 17535  Grpcgrp 17623  invgcminusg 17624  SymGrpcsymg 17997  pmTrspcpmtr 18061  pmSgncpsgn 18109  pmEvencevpm 18110  mulGrpcmgp 18689  1rcur 18701  Ringcrg 18747  ℤRHomczrh 20050   Mat cmat 20415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-xor 1614  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-ot 4330  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-tpos 7521  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-sup 8513  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-xnn0 11556  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-hash 13312  df-word 13485  df-lsw 13486  df-concat 13487  df-s1 13488  df-substr 13489  df-splice 13490  df-reverse 13491  df-s2 13793  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-0g 16304  df-gsum 16305  df-prds 16310  df-pws 16312  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-mulg 17742  df-subg 17792  df-ghm 17859  df-gim 17902  df-oppg 17976  df-symg 17998  df-pmtr 18062  df-psgn 18111  df-evpm 18112  df-cmn 18395  df-abl 18396  df-mgp 18690  df-ur 18702  df-ring 18749  df-cring 18750  df-oppr 18823  df-dvdsr 18841  df-unit 18842  df-invr 18872  df-dvr 18883  df-rnghom 18917  df-drng 18951  df-subrg 18980  df-sra 19374  df-rgmod 19375  df-cnfld 19949  df-zring 20021  df-zrh 20054  df-dsmm 20278  df-frlm 20293  df-mat 20416
This theorem is referenced by:  mdetunilem8  20627
  Copyright terms: Public domain W3C validator