mdetunilem7 - Metamath Proof Explorer

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

Theorem mdetunilem7 22988

Description: Lemma for mdetuni 22992. (Contributed by SO, 15-Jul-2018.)

**Hypotheses**
Ref	Expression
mdetuni.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetuni.b	⊢ 𝐵 = (Base‘𝐴)
mdetuni.k	⊢ 𝐾 = (Base‘𝑅)
mdetuni.0g	⊢ 0 = (0_g‘𝑅)
mdetuni.1r	⊢ 1 = (1_r‘𝑅)
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-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏))) = ((((ℤ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.

Step	Hyp	Ref	Expression
1		fveq1 6915	. . . . . 6 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑎) = (𝑑‘𝑎))
2	1	oveq1d 7466	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝑐‘𝑎)𝐹𝑏) = ((𝑑‘𝑎)𝐹𝑏))
3	2	mpoeq3dv 7530	. . . 4 ⊢ (𝑐 = 𝑑 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))
4	3	fveq2d 6920	. . 3 ⊢ (𝑐 = 𝑑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))))
5		fveq2 6916	. . . 4 ⊢ (𝑐 = 𝑑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑))
6	5	oveq1d 7466	. . 3 ⊢ (𝑐 = 𝑑 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹)))
7	4, 6	eqeq12d 2779	. 2 ⊢ (𝑐 = 𝑑 → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) ↔ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))))
8		fveq1 6915	. . . . . 6 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → (𝑐‘𝑎) = ((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎))
9	8	oveq1d 7466	. . . . 5 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → ((𝑐‘𝑎)𝐹𝑏) = (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))
10	9	mpoeq3dv 7530	. . . 4 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)))
11	10	fveq2d 6920	. . 3 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))))
12		fveq2 6916	. . . 4 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)))
13	12	oveq1d 7466	. . 3 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) · (𝐷‘𝐹)))
14	11, 13	eqeq12d 2779	. 2 ⊢ (𝑐 = (𝑑(+_g‘(SymGrp‘𝑁))𝑒) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) ↔ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) · (𝐷‘𝐹))))
15		fveq1 6915	. . . . . 6 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → (𝑐‘𝑎) = ((0_g‘(SymGrp‘𝑁))‘𝑎))
16	15	oveq1d 7466	. . . . 5 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → ((𝑐‘𝑎)𝐹𝑏) = (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))
17	16	mpoeq3dv 7530	. . . 4 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)))
18	17	fveq2d 6920	. . 3 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))))
19		fveq2 6916	. . . 4 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))))
20	19	oveq1d 7466	. . 3 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) · (𝐷‘𝐹)))
21	18, 20	eqeq12d 2779	. 2 ⊢ (𝑐 = (0_g‘(SymGrp‘𝑁)) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) ↔ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) · (𝐷‘𝐹))))
22		fveq1 6915	. . . . . 6 ⊢ (𝑐 = 𝐸 → (𝑐‘𝑎) = (𝐸‘𝑎))
23	22	oveq1d 7466	. . . . 5 ⊢ (𝑐 = 𝐸 → ((𝑐‘𝑎)𝐹𝑏) = ((𝐸‘𝑎)𝐹𝑏))
24	23	mpoeq3dv 7530	. . . 4 ⊢ (𝑐 = 𝐸 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏)))
25	24	fveq2d 6920	. . 3 ⊢ (𝑐 = 𝐸 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏))))
26		fveq2 6916	. . . 4 ⊢ (𝑐 = 𝐸 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸))
27	26	oveq1d 7466	. . 3 ⊢ (𝑐 = 𝐸 → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷‘𝐹)))
28	25, 27	eqeq12d 2779	. 2 ⊢ (𝑐 = 𝐸 → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑐‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑐) · (𝐷‘𝐹)) ↔ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷‘𝐹))))
29		eqid 2763	. 2 ⊢ (0_g‘(SymGrp‘𝑁)) = (0_g‘(SymGrp‘𝑁))
30		eqid 2763	. 2 ⊢ (+_g‘(SymGrp‘𝑁)) = (+_g‘(SymGrp‘𝑁))
31		eqid 2763	. 2 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
32		mdetuni.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ Fin)
33	32	3ad2ant1 1151	. . 3 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝑁 ∈ Fin)
34		eqid 2763	. . . 4 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
35	34	symggrp 19665	. . 3 ⊢ (𝑁 ∈ Fin → (SymGrp‘𝑁) ∈ Grp)
36		grpmnd 19201	. . 3 ⊢ ((SymGrp‘𝑁) ∈ Grp → (SymGrp‘𝑁) ∈ Mnd)
37	33, 35, 36	3syl 19	. 2 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (SymGrp‘𝑁) ∈ Mnd)
38		eqid 2763	. . . 4 ⊢ ran (pmTrsp‘𝑁) = ran (pmTrsp‘𝑁)
39	38, 34, 31	symgtrf 19734	. . 3 ⊢ ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁))
40	39	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → ran (pmTrsp‘𝑁) ⊆ (Base‘(SymGrp‘𝑁)))
41		eqid 2763	. . . . . 6 ⊢ (mrCls‘(SubMnd‘(SymGrp‘𝑁))) = (mrCls‘(SubMnd‘(SymGrp‘𝑁)))
42	38, 34, 31, 41	symggen2 19736	. . . . 5 ⊢ (𝑁 ∈ Fin → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
43	32, 42	syl 18	. . . 4 ⊢ (𝜑 → ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)) = (Base‘(SymGrp‘𝑁)))
44	43	eqcomd 2769	. . 3 ⊢ (𝜑 → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
45	44	3ad2ant1 1151	. 2 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = ((mrCls‘(SubMnd‘(SymGrp‘𝑁)))‘ran (pmTrsp‘𝑁)))
46		mdetuni.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
47	46	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝑅 ∈ Ring)
48		mdetuni.ff	. . . . . 6 ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)
49	48	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐷:𝐵⟶𝐾)
50		simp3 1156	. . . . 5 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐹 ∈ 𝐵)
51	49, 50	ffvelcdmd 7117	. . . 4 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘𝐹) ∈ 𝐾)
52		mdetuni.k	. . . . 5 ⊢ 𝐾 = (Base‘𝑅)
53		mdetuni.tg	. . . . 5 ⊢ · = (._r‘𝑅)
54		mdetuni.1r	. . . . 5 ⊢ 1 = (1_r‘𝑅)
55	52, 53, 54	ringlidm 20549	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝐷‘𝐹) ∈ 𝐾) → ( 1 · (𝐷‘𝐹)) = (𝐷‘𝐹))
56	47, 51, 55	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → ( 1 · (𝐷‘𝐹)) = (𝐷‘𝐹))
57		zrhpsgnmhm 21945	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
58	46, 32, 57	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
59		eqid 2763	. . . . . . . 8 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
60	59, 54	ringidval 20460	. . . . . . 7 ⊢ 1 = (0_g‘(mulGrp‘𝑅))
61	29, 60	mhm0 19039	. . . . . 6 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) = 1 )
62	58, 61	syl 18	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) = 1 )
63	62	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) = 1 )
64	63	oveq1d 7466	. . 3 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) · (𝐷‘𝐹)) = ( 1 · (𝐷‘𝐹)))
65	34	symgid 19666	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ Fin → ( I ↾ 𝑁) = (0_g‘(SymGrp‘𝑁)))
66	32, 65	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ( I ↾ 𝑁) = (0_g‘(SymGrp‘𝑁)))
67	66	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → ( I ↾ 𝑁) = (0_g‘(SymGrp‘𝑁)))
68	67	3ad2ant1 1151	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ( I ↾ 𝑁) = (0_g‘(SymGrp‘𝑁)))
69	68	fveq1d 6918	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (( I ↾ 𝑁)‘𝑎) = ((0_g‘(SymGrp‘𝑁))‘𝑎))
70		simp2 1155	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑎 ∈ 𝑁)
71		fvresi 7209	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝑁 → (( I ↾ 𝑁)‘𝑎) = 𝑎)
72	70, 71	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (( I ↾ 𝑁)‘𝑎) = 𝑎)
73	69, 72	eqtr3d 2800	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((0_g‘(SymGrp‘𝑁))‘𝑎) = 𝑎)
74	73	oveq1d 7466	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏) = (𝑎𝐹𝑏))
75	74	mpoeq3dva 7528	. . . . 5 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (𝑎𝐹𝑏)))
76		mdetuni.a	. . . . . . . . 9 ⊢ 𝐴 = (𝑁 Mat 𝑅)
77		mdetuni.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐴)
78	76, 52, 77	matbas2i 22792	. . . . . . . 8 ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (𝐾 ↑_m (𝑁 × 𝑁)))
79	78	3ad2ant3 1153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐹 ∈ (𝐾 ↑_m (𝑁 × 𝑁)))
80		elmapi 8907	. . . . . . 7 ⊢ (𝐹 ∈ (𝐾 ↑_m (𝑁 × 𝑁)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
81		ffn 6739	. . . . . . 7 ⊢ (𝐹:(𝑁 × 𝑁)⟶𝐾 → 𝐹 Fn (𝑁 × 𝑁))
82	79, 80, 81	3syl 19	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐹 Fn (𝑁 × 𝑁))
83		fnov 7582	. . . . . 6 ⊢ (𝐹 Fn (𝑁 × 𝑁) ↔ 𝐹 = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (𝑎𝐹𝑏)))
84	82, 83	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐹 = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (𝑎𝐹𝑏)))
85	75, 84	eqtr4d 2801	. . . 4 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏)) = 𝐹)
86	85	fveq2d 6920	. . 3 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = (𝐷‘𝐹))
87	56, 64, 86	3eqtr4rd 2809	. 2 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((0_g‘(SymGrp‘𝑁))‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(0_g‘(SymGrp‘𝑁))) · (𝐷‘𝐹)))
88		simp2 1155	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑑 ∈ (Base‘(SymGrp‘𝑁)))
89	39	sseli 3909	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ ran (pmTrsp‘𝑁) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
90	89	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ (Base‘(SymGrp‘𝑁)))
91	34, 31, 30	symgov 19649	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (𝑑(+_g‘(SymGrp‘𝑁))𝑒) = (𝑑 ∘ 𝑒))
92	88, 90, 91	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑑(+_g‘(SymGrp‘𝑁))𝑒) = (𝑑 ∘ 𝑒))
93	92	fveq1d 6918	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑 ∘ 𝑒)‘𝑎))
94	93	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎) = ((𝑑 ∘ 𝑒)‘𝑎))
95	34, 31	symgbasf1o 19640	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ (Base‘(SymGrp‘𝑁)) → 𝑒:𝑁⟶1-1onto𝑁)
96		f1of 6854	. . . . . . . . . . . 12 ⊢ (𝑒:𝑁⟶1-1onto𝑁 → 𝑒:𝑁⟶𝑁)
97	90, 95, 96	3syl 19	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒:𝑁⟶𝑁)
98	97	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑒:𝑁⟶𝑁)
99		simp2 1155	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑎 ∈ 𝑁)
100		fvco3 7016	. . . . . . . . . 10 ⊢ ((𝑒:𝑁⟶𝑁 ∧ 𝑎 ∈ 𝑁) → ((𝑑 ∘ 𝑒)‘𝑎) = (𝑑‘(𝑒‘𝑎)))
101	98, 99, 100	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑑 ∘ 𝑒)‘𝑎) = (𝑑‘(𝑒‘𝑎)))
102	94, 101	eqtrd 2798	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎) = (𝑑‘(𝑒‘𝑎)))
103	102	oveq1d 7466	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏) = ((𝑑‘(𝑒‘𝑎))𝐹𝑏))
104	103	mpoeq3dva 7528	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏)))
105	104	fveq2d 6920	. . . . 5 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))))
106	34, 31	symgbasf 19641	. . . . . 6 ⊢ (𝑑 ∈ (Base‘(SymGrp‘𝑁)) → 𝑑:𝑁⟶𝑁)
107		eqid 2763	. . . . . . . . 9 ⊢ (pmTrsp‘𝑁) = (pmTrsp‘𝑁)
108	107, 38	pmtrrn2 19725	. . . . . . . 8 ⊢ (𝑒 ∈ ran (pmTrsp‘𝑁) → ∃𝑐 ∈ 𝑁 ∃𝑓 ∈ 𝑁 (𝑐 ≠ 𝑓 ∧ 𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})))
109		mdetuni.0g	. . . . . . . . . . . . . 14 ⊢ 0 = (0_g‘𝑅)
110		mdetuni.pg	. . . . . . . . . . . . . 14 ⊢ + = (+_g‘𝑅)
111		mdetuni.al	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))
112		mdetuni.li	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))
113		mdetuni.sc	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))
114		simpll1 1231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝜑)
115		df-3an 1105	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓) ↔ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓))
116	115	bilanri 512	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓))
117	79, 80	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
118	117	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
119	118	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
120		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → 𝑑:𝑁⟶𝑁)
121		simprlr 792	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝑓 ∈ 𝑁)
122	121	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → 𝑓 ∈ 𝑁)
123	120, 122	ffvelcdmd 7117	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → (𝑑‘𝑓) ∈ 𝑁)
124		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁)
125	119, 123, 124	fovcdmd 7625	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → ((𝑑‘𝑓)𝐹𝑏) ∈ 𝐾)
126		simprll 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝑐 ∈ 𝑁)
127	126	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → 𝑐 ∈ 𝑁)
128	120, 127	ffvelcdmd 7117	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → (𝑑‘𝑐) ∈ 𝑁)
129	119, 128, 124	fovcdmd 7625	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → ((𝑑‘𝑐)𝐹𝑏) ∈ 𝐾)
130	125, 129	jca 521	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑏 ∈ 𝑁) → (((𝑑‘𝑓)𝐹𝑏) ∈ 𝐾 ∧ ((𝑑‘𝑐)𝐹𝑏) ∈ 𝐾))
131	117	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
132	131	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐹:(𝑁 × 𝑁)⟶𝐾)
133		simp1lr 1256	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑑:𝑁⟶𝑁)
134		simp2 1155	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑎 ∈ 𝑁)
135	133, 134	ffvelcdmd 7117	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑑‘𝑎) ∈ 𝑁)
136		simp3 1156	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁)
137	132, 135, 136	fovcdmd 7625	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑑‘𝑎)𝐹𝑏) ∈ 𝐾)
138	76, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 116, 130, 137	mdetunilem6 22987	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))))))
139		simpl1 1210	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) → 𝜑)
140		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑐 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐))
141	32	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝑁 ∈ Fin)
142		simprll 791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝑐 ∈ 𝑁)
143		simprlr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝑓 ∈ 𝑁)
144		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → 𝑐 ≠ 𝑓)
145	107	pmtrprfv 19718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ Fin ∧ (𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁 ∧ 𝑐 ≠ 𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
146	141, 142, 143, 144, 145	syl13anc 1400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
147	146	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑐) = 𝑓)
148	140, 147	sylan9eqr 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑐) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑓)
149	148	fveq2d 6920	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑐) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑‘𝑓))
150	149	oveq1d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑‘𝑓)𝐹𝑏))
151		iftrue 4491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))) = ((𝑑‘𝑓)𝐹𝑏))
152	151	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))) = ((𝑑‘𝑓)𝐹𝑏))
153	150, 152	eqtr4d 2801	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
154		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑓 → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓))
155		prcom 4695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑐, 𝑓} = {𝑓, 𝑐}
156	155	fveq2i 6919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) = ((pmTrsp‘𝑁)‘{𝑓, 𝑐})
157	156	fveq1i 6917	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓)
158	32	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ Fin)
159		simplrl 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → (𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁))
160	159	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → 𝑓 ∈ 𝑁)
161	159	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → 𝑐 ∈ 𝑁)
162		simplrr 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → 𝑐 ≠ 𝑓)
163	162	necomd 3014	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → 𝑓 ≠ 𝑐)
164	107	pmtrprfv 19718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ Fin ∧ (𝑓 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ∧ 𝑓 ≠ 𝑐)) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
165	158, 160, 161, 163, 164	syl13anc 1400	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝑓, 𝑐})‘𝑓) = 𝑐)
166	157, 165	eqtrid 2810	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑓) = 𝑐)
167	154, 166	sylan9eqr 2820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑐)
168	167	fveq2d 6920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑‘𝑐))
169	168	oveq1d 7466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑‘𝑐)𝐹𝑏))
170		iftrue 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)) = ((𝑑‘𝑐)𝐹𝑏))
171	170	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)) = ((𝑑‘𝑐)𝐹𝑏))
172	169, 171	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
173	172	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
174		vex 3458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑎 ∈ V
175	174	elpr 4609	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 ∈ {𝑐, 𝑓} ↔ (𝑎 = 𝑐 ∨ 𝑎 = 𝑓))
176	175	notbii 323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑎 ∈ {𝑐, 𝑓} ↔ ¬ (𝑎 = 𝑐 ∨ 𝑎 = 𝑓))
177		ioran 999	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ (𝑎 = 𝑐 ∨ 𝑎 = 𝑓) ↔ (¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓))
178	176, 177	sylbbr 239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
179	178	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ {𝑐, 𝑓})
180		prssi 4782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
181	159, 180	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → {𝑐, 𝑓} ⊆ 𝑁)
182		pr2ne 10123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) → ({𝑐, 𝑓} ≈ 2_o ↔ 𝑐 ≠ 𝑓))
183	159, 182	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → ({𝑐, 𝑓} ≈ 2_o ↔ 𝑐 ≠ 𝑓))
184	162, 183	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → {𝑐, 𝑓} ≈ 2_o)
185	107	pmtrmvd 19721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2_o) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
186	158, 181, 184, 185	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) = {𝑐, 𝑓})
187	186	eleq2d 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ 𝑎 ∈ {𝑐, 𝑓}))
188	187	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
189	188	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ ¬ 𝑎 ∈ {𝑐, 𝑓}))
190	179, 189	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ))
191	107	pmtrf 19720	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ Fin ∧ {𝑐, 𝑓} ⊆ 𝑁 ∧ {𝑐, 𝑓} ≈ 2_o) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁⟶𝑁)
192	158, 181, 184, 191	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}):𝑁⟶𝑁)
193	192	ffnd 6740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁)
194		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → 𝑎 ∈ 𝑁)
195		fnelnfp 7213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁 ∧ 𝑎 ∈ 𝑁) → (𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I ) ↔ (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) ≠ 𝑎))
196	195	necon2bbid 3002	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((pmTrsp‘𝑁)‘{𝑐, 𝑓}) Fn 𝑁 ∧ 𝑎 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
197	193, 194, 196	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
198	197	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎 ↔ ¬ 𝑎 ∈ dom (((pmTrsp‘𝑁)‘{𝑐, 𝑓}) ∖ I )))
199	190, 198	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎) = 𝑎)
200	199	fveq2d 6920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)) = (𝑑‘𝑎))
201	200	oveq1d 7466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = ((𝑑‘𝑎)𝐹𝑏))
202		iffalse 4494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)) = ((𝑑‘𝑎)𝐹𝑏))
203	202	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)) = ((𝑑‘𝑎)𝐹𝑏))
204	201, 203	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
205	173, 204	pm2.61dan 825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
206		iffalse 4494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
207	206	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) → if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
208	205, 207	eqtr4d 2801	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑐) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
209	153, 208	pm2.61dan 825	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
210	209	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
211	210	mpoeq3dva 7528	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))))
212	139, 211	sylan 592	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))))
213	212	fveq2d 6920	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑓)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑐)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))))
214		fveq2 6916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑑‘𝑎) = (𝑑‘𝑐))
215	214	oveq1d 7466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → ((𝑑‘𝑎)𝐹𝑏) = ((𝑑‘𝑐)𝐹𝑏))
216		iftrue 4491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))) = ((𝑑‘𝑐)𝐹𝑏))
217	215, 216	eqtr4d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
218		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑓 → (𝑑‘𝑎) = (𝑑‘𝑓))
219	218	oveq1d 7466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → ((𝑑‘𝑎)𝐹𝑏) = ((𝑑‘𝑓)𝐹𝑏))
220		iftrue 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)) = ((𝑑‘𝑓)𝐹𝑏))
221	219, 220	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑓 → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
222	221	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑎 = 𝑐 ∧ 𝑎 = 𝑓) → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
223		iffalse 4494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑎 = 𝑓 → if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)) = ((𝑑‘𝑎)𝐹𝑏))
224	223	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑎 = 𝑓 → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
225	224	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑎 = 𝑐 ∧ ¬ 𝑎 = 𝑓) → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
226	222, 225	pm2.61dan 825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑎 = 𝑐 → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
227		iffalse 4494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑎 = 𝑐 → if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))) = if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
228	226, 227	eqtr4d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑎 = 𝑐 → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
229	217, 228	pm2.61i 184	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))
230	229	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑑‘𝑎)𝐹𝑏) = if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
231	230	mpoeq3ia 7529	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))
232	231	fveq2i 6919	. . . . . . . . . . . . . . 15 ⊢ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))))
233	232	fveq2i 6919	. . . . . . . . . . . . . 14 ⊢ ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏))))))
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑐, ((𝑑‘𝑐)𝐹𝑏), if(𝑎 = 𝑓, ((𝑑‘𝑓)𝐹𝑏), ((𝑑‘𝑎)𝐹𝑏)))))))
235	138, 213, 234	3eqtr4d 2808	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))))
236		fveq1 6915	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑒‘𝑎) = (((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))
237	236	fveq2d 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑑‘(𝑒‘𝑎)) = (𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎)))
238	237	oveq1d 7466	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝑑‘(𝑒‘𝑎))𝐹𝑏) = ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))
239	238	mpoeq3dv 7530	. . . . . . . . . . . . 13 ⊢ (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏)))
240	239	fveqeq2d 6924	. . . . . . . . . . . 12 ⊢ (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))) ↔ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(((pmTrsp‘𝑁)‘{𝑐, 𝑓})‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))))))
241	235, 240	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ ((𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁) ∧ 𝑐 ≠ 𝑓)) → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))))))
242	241	expr 462	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ (𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁)) → (𝑐 ≠ 𝑓 → (𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))))))
243	242	impd 416	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) ∧ (𝑐 ∈ 𝑁 ∧ 𝑓 ∈ 𝑁)) → ((𝑐 ≠ 𝑓 ∧ 𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))))))
244	243	rexlimdvva 3223	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) → (∃𝑐 ∈ 𝑁 ∃𝑓 ∈ 𝑁 (𝑐 ≠ 𝑓 ∧ 𝑒 = ((pmTrsp‘𝑁)‘{𝑐, 𝑓})) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))))))
245	108, 244	syl5 35	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁) → (𝑒 ∈ ran (pmTrsp‘𝑁) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))))))
246	245	3impia 1135	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑:𝑁⟶𝑁 ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))))
247	106, 246	syl3an2 1182	. . . . 5 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘(𝑒‘𝑎))𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))))
248	105, 247	eqtrd 2798	. . . 4 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))))
249	248	adantr 486	. . 3 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))))
250		fveq2 6916	. . . 4 ⊢ ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹)) → ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))) = ((inv_g‘𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))))
251	250	adantl 487	. . 3 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))) → ((inv_g‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏)))) = ((inv_g‘𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))))
252		eqid 2763	. . . . . 6 ⊢ (inv_g‘𝑅) = (inv_g‘𝑅)
253	47	3ad2ant1 1151	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑅 ∈ Ring)
254	58	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
255	254	3ad2ant1 1151	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
256	59, 52	mgpbas 20416	. . . . . . . . 9 ⊢ 𝐾 = (Base‘(mulGrp‘𝑅))
257	31, 256	mhmf 19034	. . . . . . . 8 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
258	255, 257	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
259	258, 88	ffvelcdmd 7117	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) ∈ 𝐾)
260	49	3ad2ant1 1151	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐷:𝐵⟶𝐾)
261		simp13 1224	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝐹 ∈ 𝐵)
262	260, 261	ffvelcdmd 7117	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (𝐷‘𝐹) ∈ 𝐾)
263	52, 53, 252, 253, 259, 262	ringmneg1 20586	. . . . 5 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((inv_g‘𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷‘𝐹)) = ((inv_g‘𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))))
264	59, 53	mgpplusg 20415	. . . . . . . . 9 ⊢ · = (+_g‘(mulGrp‘𝑅))
265	31, 30, 264	mhmlin 19038	. . . . . . . 8 ⊢ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
266	255, 88, 90, 265	syl3anc 1399	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)))
267	33	3ad2ant1 1151	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑁 ∈ Fin)
268		simp3 1156	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ran (pmTrsp‘𝑁))
269	34, 31, 38	pmtrodpm 21958	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
270	267, 268, 269	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁)))
271		eqid 2763	. . . . . . . . . 10 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
272		eqid 2763	. . . . . . . . . 10 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
273	271, 272, 54, 31, 252	zrhpsgnodpm 21953	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑒 ∈ ((Base‘(SymGrp‘𝑁)) ∖ (pmEven‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((inv_g‘𝑅)‘ 1 ))
274	253, 267, 270, 273	syl3anc 1399	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒) = ((inv_g‘𝑅)‘ 1 ))
275	274	oveq2d 7467	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑒)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((inv_g‘𝑅)‘ 1 )))
276	52, 53, 54, 252, 253, 259	ringnegr 20585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · ((inv_g‘𝑅)‘ 1 )) = ((inv_g‘𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)))
277	266, 275, 276	3eqtrrd 2803	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((inv_g‘𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)))
278	277	oveq1d 7466	. . . . 5 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → (((inv_g‘𝑅)‘(((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑)) · (𝐷‘𝐹)) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) · (𝐷‘𝐹)))
279	263, 278	eqtr3d 2800	. . . 4 ⊢ (((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) → ((inv_g‘𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) · (𝐷‘𝐹)))
280	279	adantr 486	. . 3 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))) → ((inv_g‘𝑅)‘((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) · (𝐷‘𝐹)))
281	249, 251, 280	3eqtrd 2802	. 2 ⊢ ((((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) ∧ 𝑑 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑒 ∈ ran (pmTrsp‘𝑁)) ∧ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝑑‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑑) · (𝐷‘𝐹))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (((𝑑(+_g‘(SymGrp‘𝑁))𝑒)‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘(𝑑(+_g‘(SymGrp‘𝑁))𝑒)) · (𝐷‘𝐹)))
282		simp2 1155	. . 3 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐸:𝑁⟶1-1onto𝑁)
283	34, 31	elsymgbas 19639	. . . 4 ⊢ (𝑁 ∈ Fin → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁⟶1-1onto𝑁))
284	33, 283	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐸 ∈ (Base‘(SymGrp‘𝑁)) ↔ 𝐸:𝑁⟶1-1onto𝑁))
285	282, 284	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → 𝐸 ∈ (Base‘(SymGrp‘𝑁)))
286	7, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 281, 285	mndind 19074	1 ⊢ ((𝜑 ∧ 𝐸:𝑁⟶1-1onto𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷‘𝐹)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ∖ cdif 4048 ifcif 4485 {csn 4588 {cpr 4590 class class class wbr 5108 I cid 5552 × cxp 5656 dom cdm 5658 ran crn 5659 ↾ cres 5660 ∘ ccom 5662 Fn wfn 6561 ⟶wf 6562 ⟶1-1ontowf1o 6565 ‘cfv 6566 (class class class)co 7451 ∈ cmpo 7453 ∘_f cof 7723 2_oc2o 8508 ↑_m cmap 8885 ≈ cen 9008 Fincfn 9011 Basecbs 17431 +_gcplusg 17472 ._rcmulr 17473 0_gc0g 17660 mrClscmrc 17803 Mndcmnd 18973 MndHom cmhm 19026 SubMndcsubmnd 19027 Grpcgrp 19194 inv_gcminusg 19195 SymGrpcsymg 19634 pmTrspcpmtr 19706 pmSgncpsgn 19754 pmEvencevpm 19755 mulGrpcmgp 20411 1_rcur 20458 Ringcrg 20510 ℤRHomczrh 21860 Mat cmat 22777

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-addf 11318 ax-mulf 11319

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-ot 4864 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-tpos 8281 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-sup 9471 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-xnn0 12720 df-z 12734 df-dec 12855 df-uz 13006 df-rp 13161 df-fz 13680 df-fzo 13829 df-seq 14185 df-exp 14245 df-hash 14516 df-word 14700 df-lsw 14749 df-concat 14757 df-s1 14784 df-substr 14831 df-pfx 14863 df-splice 14941 df-reverse 14950 df-s2 15041 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-0g 17662 df-gsum 17663 df-prds 17668 df-pws 17670 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-mhm 19028 df-submnd 19029 df-efmnd 19115 df-grp 19197 df-minusg 19198 df-mulg 19328 df-subg 19383 df-ghm 19478 df-gim 19523 df-oppg 19611 df-symg 19635 df-pmtr 19707 df-psgn 19756 df-evpm 19757 df-cmn 20047 df-abl 20048 df-mgp 20412 df-rng 20426 df-ur 20459 df-ring 20512 df-cring 20513 df-oppr 20618 df-dvdsr 20638 df-unit 20639 df-invr 20669 df-dvr 20682 df-rhm 20753 df-subrng 20849 df-subrg 20873 df-drng 21033 df-sra 21499 df-rgmod 21500 df-cnfld 21730 df-zring 21807 df-zrh 21864 df-dsmm 22093 df-frlm 22108 df-mat 22778

This theorem is used by: mdetunilem8 22989

W3C validator