Metamath Proof Explorer

Theorem mdetunilem7

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

Ref Expression
Hypotheses mdetuni.a ⊢ A = N Mat R
mdetuni.b ⊢ B = Base A
mdetuni.k ⊢ K = Base R
mdetuni.0g ⊢ 0 ˙ = 0 R
mdetuni.1r ⊢ 1 ˙ = 1 R
mdetuni.pg ⊢ + ˙ = + R
mdetuni.tg ⊢ · ˙ = ⋅ R
mdetuni.n ⊢ φ → N ∈ Fin
mdetuni.r ⊢ φ → R ∈ Ring
mdetuni.ff ⊢ φ → D : B ⟶ K
mdetuni.al ⊢ φ → ∀ x ∈ B ∀ y ∈ N ∀ z ∈ N y ≠ z ∧ ∀ w ∈ N y x w = z x w → D ⁡ x = 0 ˙
mdetuni.li ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
mdetuni.sc ⊢ φ → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
Assertion mdetunilem7 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → D ⁡ a ∈ N , b ∈ N ⟼ E ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ E · ˙ D ⁡ F

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢ A = N Mat R
2 mdetuni.b ⊢ B = Base A
3 mdetuni.k ⊢ K = Base R
4 mdetuni.0g ⊢ 0 ˙ = 0 R
5 mdetuni.1r ⊢ 1 ˙ = 1 R
6 mdetuni.pg ⊢ + ˙ = + R
7 mdetuni.tg ⊢ · ˙ = ⋅ R
8 mdetuni.n ⊢ φ → N ∈ Fin
9 mdetuni.r ⊢ φ → R ∈ Ring
10 mdetuni.ff ⊢ φ → D : B ⟶ K
11 mdetuni.al ⊢ φ → ∀ x ∈ B ∀ y ∈ N ∀ z ∈ N y ≠ z ∧ ∀ w ∈ N y x w = z x w → D ⁡ x = 0 ˙
12 mdetuni.li ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
13 mdetuni.sc ⊢ φ → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
14 fveq1 ⊢ c = d → c ⁡ a = d ⁡ a
15 14 oveq1d ⊢ c = d → c ⁡ a F b = d ⁡ a F b
16 15 mpoeq3dv ⊢ c = d → a ∈ N , b ∈ N ⟼ c ⁡ a F b = a ∈ N , b ∈ N ⟼ d ⁡ a F b
17 16 fveq2d ⊢ c = d → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
18 fveq2 ⊢ c = d → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d
19 18 oveq1d ⊢ c = d → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F
20 17 19 eqeq12d ⊢ c = d → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F ↔ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F
21 fveq1 ⊢ c = d + SymGrp ⁡ N e → c ⁡ a = d + SymGrp ⁡ N e ⁡ a
22 21 oveq1d ⊢ c = d + SymGrp ⁡ N e → c ⁡ a F b = d + SymGrp ⁡ N e ⁡ a F b
23 22 mpoeq3dv ⊢ c = d + SymGrp ⁡ N e → a ∈ N , b ∈ N ⟼ c ⁡ a F b = a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b
24 23 fveq2d ⊢ c = d + SymGrp ⁡ N e → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b
25 fveq2 ⊢ c = d + SymGrp ⁡ N e → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e
26 25 oveq1d ⊢ c = d + SymGrp ⁡ N e → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e · ˙ D ⁡ F
27 24 26 eqeq12d ⊢ c = d + SymGrp ⁡ N e → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F ↔ D ⁡ a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e · ˙ D ⁡ F
28 fveq1 ⊢ c = 0 SymGrp ⁡ N → c ⁡ a = 0 SymGrp ⁡ N ⁡ a
29 28 oveq1d ⊢ c = 0 SymGrp ⁡ N → c ⁡ a F b = 0 SymGrp ⁡ N ⁡ a F b
30 29 mpoeq3dv ⊢ c = 0 SymGrp ⁡ N → a ∈ N , b ∈ N ⟼ c ⁡ a F b = a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b
31 30 fveq2d ⊢ c = 0 SymGrp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b
32 fveq2 ⊢ c = 0 SymGrp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N
33 32 oveq1d ⊢ c = 0 SymGrp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N · ˙ D ⁡ F
34 31 33 eqeq12d ⊢ c = 0 SymGrp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F ↔ D ⁡ a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N · ˙ D ⁡ F
35 fveq1 ⊢ c = E → c ⁡ a = E ⁡ a
36 35 oveq1d ⊢ c = E → c ⁡ a F b = E ⁡ a F b
37 36 mpoeq3dv ⊢ c = E → a ∈ N , b ∈ N ⟼ c ⁡ a F b = a ∈ N , b ∈ N ⟼ E ⁡ a F b
38 37 fveq2d ⊢ c = E → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ E ⁡ a F b
39 fveq2 ⊢ c = E → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ E
40 39 oveq1d ⊢ c = E → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ E · ˙ D ⁡ F
41 38 40 eqeq12d ⊢ c = E → D ⁡ a ∈ N , b ∈ N ⟼ c ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ c · ˙ D ⁡ F ↔ D ⁡ a ∈ N , b ∈ N ⟼ E ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ E · ˙ D ⁡ F
42 eqid ⊢ 0 SymGrp ⁡ N = 0 SymGrp ⁡ N
43 eqid ⊢ + SymGrp ⁡ N = + SymGrp ⁡ N
44 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
45 8 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → N ∈ Fin
46 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
47 46 symggrp ⊢ N ∈ Fin → SymGrp ⁡ N ∈ Grp
48 grpmnd ⊢ SymGrp ⁡ N ∈ Grp → SymGrp ⁡ N ∈ Mnd
49 45 47 48 3syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → SymGrp ⁡ N ∈ Mnd
50 eqid ⊢ ran ⁡ pmTrsp ⁡ N = ran ⁡ pmTrsp ⁡ N
51 50 46 44 symgtrf ⊢ ran ⁡ pmTrsp ⁡ N ⊆ Base SymGrp ⁡ N
52 51 a1i ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → ran ⁡ pmTrsp ⁡ N ⊆ Base SymGrp ⁡ N
53 eqid ⊢ mrCls ⁡ SubMnd ⁡ SymGrp ⁡ N = mrCls ⁡ SubMnd ⁡ SymGrp ⁡ N
54 50 46 44 53 symggen2 ⊢ N ∈ Fin → mrCls ⁡ SubMnd ⁡ SymGrp ⁡ N ⁡ ran ⁡ pmTrsp ⁡ N = Base SymGrp ⁡ N
55 8 54 syl ⊢ φ → mrCls ⁡ SubMnd ⁡ SymGrp ⁡ N ⁡ ran ⁡ pmTrsp ⁡ N = Base SymGrp ⁡ N
56 55 eqcomd ⊢ φ → Base SymGrp ⁡ N = mrCls ⁡ SubMnd ⁡ SymGrp ⁡ N ⁡ ran ⁡ pmTrsp ⁡ N
57 56 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → Base SymGrp ⁡ N = mrCls ⁡ SubMnd ⁡ SymGrp ⁡ N ⁡ ran ⁡ pmTrsp ⁡ N
58 9 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → R ∈ Ring
59 10 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → D : B ⟶ K
60 simp3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → F ∈ B
61 59 60 ffvelcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → D ⁡ F ∈ K
62 3 7 5 ringlidm ⊢ R ∈ Ring ∧ D ⁡ F ∈ K → 1 ˙ · ˙ D ⁡ F = D ⁡ F
63 58 61 62 syl2anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → 1 ˙ · ˙ D ⁡ F = D ⁡ F
64 zrhpsgnmhm ⊢ R ∈ Ring ∧ N ∈ Fin → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
65 9 8 64 syl2anc ⊢ φ → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
66 eqid ⊢ mulGrp R = mulGrp R
67 66 5 ringidval ⊢ 1 ˙ = 0 mulGrp R
68 42 67 mhm0 ⊢ ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N = 1 ˙
69 65 68 syl ⊢ φ → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N = 1 ˙
70 69 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N = 1 ˙
71 70 oveq1d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N · ˙ D ⁡ F = 1 ˙ · ˙ D ⁡ F
72 46 symgid ⊢ N ∈ Fin → I ↾ N = 0 SymGrp ⁡ N
73 8 72 syl ⊢ φ → I ↾ N = 0 SymGrp ⁡ N
74 73 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → I ↾ N = 0 SymGrp ⁡ N
75 74 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ a ∈ N ∧ b ∈ N → I ↾ N = 0 SymGrp ⁡ N
76 75 fveq1d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ a ∈ N ∧ b ∈ N → I ↾ N ⁡ a = 0 SymGrp ⁡ N ⁡ a
77 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ a ∈ N ∧ b ∈ N → a ∈ N
78 fvresi ⊢ a ∈ N → I ↾ N ⁡ a = a
79 77 78 syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ a ∈ N ∧ b ∈ N → I ↾ N ⁡ a = a
80 76 79 eqtr3d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ a ∈ N ∧ b ∈ N → 0 SymGrp ⁡ N ⁡ a = a
81 80 oveq1d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ a ∈ N ∧ b ∈ N → 0 SymGrp ⁡ N ⁡ a F b = a F b
82 81 mpoeq3dva ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b = a ∈ N , b ∈ N ⟼ a F b
83 1 3 2 matbas2i ⊢ F ∈ B → F ∈ K N × N
84 83 3ad2ant3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → F ∈ K N × N
85 elmapi ⊢ F ∈ K N × N → F : N × N ⟶ K
86 ffn ⊢ F : N × N ⟶ K → F Fn N × N
87 84 85 86 3syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → F Fn N × N
88 fnov ⊢ F Fn N × N ↔ F = a ∈ N , b ∈ N ⟼ a F b
89 87 88 sylib ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → F = a ∈ N , b ∈ N ⟼ a F b
90 82 89 eqtr4d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b = F
91 90 fveq2d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → D ⁡ a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b = D ⁡ F
92 63 71 91 3eqtr4rd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → D ⁡ a ∈ N , b ∈ N ⟼ 0 SymGrp ⁡ N ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ 0 SymGrp ⁡ N · ˙ D ⁡ F
93 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → d ∈ Base SymGrp ⁡ N
94 51 sseli ⊢ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ Base SymGrp ⁡ N
95 94 3ad2ant3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ Base SymGrp ⁡ N
96 46 44 43 symgov ⊢ d ∈ Base SymGrp ⁡ N ∧ e ∈ Base SymGrp ⁡ N → d + SymGrp ⁡ N e = d ∘ e
97 93 95 96 syl2anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → d + SymGrp ⁡ N e = d ∘ e
98 97 fveq1d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → d + SymGrp ⁡ N e ⁡ a = d ∘ e ⁡ a
99 98 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ a ∈ N ∧ b ∈ N → d + SymGrp ⁡ N e ⁡ a = d ∘ e ⁡ a
100 46 44 symgbasf1o ⊢ e ∈ Base SymGrp ⁡ N → e : N ⟶ 1-1 onto N
101 f1of ⊢ e : N ⟶ 1-1 onto N → e : N ⟶ N
102 95 100 101 3syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e : N ⟶ N
103 102 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ a ∈ N ∧ b ∈ N → e : N ⟶ N
104 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ a ∈ N ∧ b ∈ N → a ∈ N
105 fvco3 ⊢ e : N ⟶ N ∧ a ∈ N → d ∘ e ⁡ a = d ⁡ e ⁡ a
106 103 104 105 syl2anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ a ∈ N ∧ b ∈ N → d ∘ e ⁡ a = d ⁡ e ⁡ a
107 99 106 eqtrd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ a ∈ N ∧ b ∈ N → d + SymGrp ⁡ N e ⁡ a = d ⁡ e ⁡ a
108 107 oveq1d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ a ∈ N ∧ b ∈ N → d + SymGrp ⁡ N e ⁡ a F b = d ⁡ e ⁡ a F b
109 108 mpoeq3dva ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b = a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b
110 109 fveq2d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b
111 46 44 symgbasf ⊢ d ∈ Base SymGrp ⁡ N → d : N ⟶ N
112 eqid ⊢ pmTrsp ⁡ N = pmTrsp ⁡ N
113 112 50 pmtrrn2 ⊢ e ∈ ran ⁡ pmTrsp ⁡ N → ∃ c ∈ N ∃ f ∈ N c ≠ f ∧ e = pmTrsp ⁡ N ⁡ c f
114 simpll1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → φ
115 df-3an ⊢ c ∈ N ∧ f ∈ N ∧ c ≠ f ↔ c ∈ N ∧ f ∈ N ∧ c ≠ f
116 115 bilanri ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N ∧ f ∈ N ∧ c ≠ f
117 84 85 syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → F : N × N ⟶ K
118 117 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N → F : N × N ⟶ K
119 118 ad2antrr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → F : N × N ⟶ K
120 simpllr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d : N ⟶ N
121 simprlr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → f ∈ N
122 121 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → f ∈ N
123 120 122 ffvelcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ f ∈ N
124 simpr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → b ∈ N
125 119 123 124 fovcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ f F b ∈ K
126 simprll ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N
127 126 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → c ∈ N
128 120 127 ffvelcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ c ∈ N
129 119 128 124 fovcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ c F b ∈ K
130 125 129 jca ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ f F b ∈ K ∧ d ⁡ c F b ∈ K
131 117 ad2antrr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → F : N × N ⟶ K
132 131 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → F : N × N ⟶ K
133 simp1lr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → d : N ⟶ N
134 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → a ∈ N
135 133 134 ffvelcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → d ⁡ a ∈ N
136 simp3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → b ∈ N
137 132 135 136 fovcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → d ⁡ a F b ∈ K
138 1 2 3 4 5 6 7 8 9 10 11 12 13 114 116 130 137 mdetunilem6 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → D ⁡ a ∈ N , b ∈ N ⟼ if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
139 simpl1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N → φ
140 fveq2 ⊢ a = c → pmTrsp ⁡ N ⁡ c f ⁡ a = pmTrsp ⁡ N ⁡ c f ⁡ c
141 8 adantr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → N ∈ Fin
142 simprll ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N
143 simprlr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → f ∈ N
144 simprr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ≠ f
145 112 pmtrprfv ⊢ N ∈ Fin ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → pmTrsp ⁡ N ⁡ c f ⁡ c = f
146 141 142 143 144 145 syl13anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → pmTrsp ⁡ N ⁡ c f ⁡ c = f
147 146 adantr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ c = f
148 140 147 sylan9eqr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → pmTrsp ⁡ N ⁡ c f ⁡ a = f
149 148 fveq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a = d ⁡ f
150 149 oveq1d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = d ⁡ f F b
151 iftrue ⊢ a = c → if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b = d ⁡ f F b
152 151 adantl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b = d ⁡ f F b
153 150 152 eqtr4d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
154 fveq2 ⊢ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = pmTrsp ⁡ N ⁡ c f ⁡ f
155 prcom ⊢ c f = f c
156 155 fveq2i ⊢ pmTrsp ⁡ N ⁡ c f = pmTrsp ⁡ N ⁡ f c
157 156 fveq1i ⊢ pmTrsp ⁡ N ⁡ c f ⁡ f = pmTrsp ⁡ N ⁡ f c ⁡ f
158 8 ad2antrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → N ∈ Fin
159 simplrl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c ∈ N ∧ f ∈ N
160 159 simprd ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → f ∈ N
161 159 simpld ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c ∈ N
162 simplrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c ≠ f
163 162 necomd ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → f ≠ c
164 112 pmtrprfv ⊢ N ∈ Fin ∧ f ∈ N ∧ c ∈ N ∧ f ≠ c → pmTrsp ⁡ N ⁡ f c ⁡ f = c
165 158 160 161 163 164 syl13anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ f c ⁡ f = c
166 157 165 eqtrid ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ f = c
167 154 166 sylan9eqr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = c
168 167 fveq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a = d ⁡ c
169 168 oveq1d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = d ⁡ c F b
170 iftrue ⊢ a = f → if a = f d ⁡ c F b d ⁡ a F b = d ⁡ c F b
171 170 adantl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → if a = f d ⁡ c F b d ⁡ a F b = d ⁡ c F b
172 169 171 eqtr4d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = f d ⁡ c F b d ⁡ a F b
173 172 adantlr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = f d ⁡ c F b d ⁡ a F b
174 vex ⊢ a ∈ V
175 174 elpr ⊢ a ∈ c f ↔ a = c ∨ a = f
176 175 notbii ⊢ ¬ a ∈ c f ↔ ¬ a = c ∨ a = f
177 ioran ⊢ ¬ a = c ∨ a = f ↔ ¬ a = c ∧ ¬ a = f
178 176 177 sylbbr ⊢ ¬ a = c ∧ ¬ a = f → ¬ a ∈ c f
179 178 adantll ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → ¬ a ∈ c f
180 prssi ⊢ c ∈ N ∧ f ∈ N → c f ⊆ N
181 159 180 syl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c f ⊆ N
182 pr2ne ⊢ c ∈ N ∧ f ∈ N → c f ≈ 2 𝑜 ↔ c ≠ f
183 159 182 syl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c f ≈ 2 𝑜 ↔ c ≠ f
184 162 183 mpbird ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c f ≈ 2 𝑜
185 112 pmtrmvd ⊢ N ∈ Fin ∧ c f ⊆ N ∧ c f ≈ 2 𝑜 → dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I = c f
186 158 181 184 185 syl3anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I = c f
187 186 eleq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ a ∈ c f
188 187 notbid ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ ¬ a ∈ c f
189 188 ad2antrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ ¬ a ∈ c f
190 179 189 mpbird ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
191 112 pmtrf ⊢ N ∈ Fin ∧ c f ⊆ N ∧ c f ≈ 2 𝑜 → pmTrsp ⁡ N ⁡ c f : N ⟶ N
192 158 181 184 191 syl3anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f : N ⟶ N
193 192 ffnd ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f Fn N
194 simpr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → a ∈ N
195 fnelnfp ⊢ pmTrsp ⁡ N ⁡ c f Fn N ∧ a ∈ N → a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ pmTrsp ⁡ N ⁡ c f ⁡ a ≠ a
196 195 necon2bbid ⊢ pmTrsp ⁡ N ⁡ c f Fn N ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ a = a ↔ ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
197 193 194 196 syl2anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ a = a ↔ ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
198 197 ad2antrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = a ↔ ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
199 190 198 mpbird ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = a
200 199 fveq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a = d ⁡ a
201 200 oveq1d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = d ⁡ a F b
202 iffalse ⊢ ¬ a = f → if a = f d ⁡ c F b d ⁡ a F b = d ⁡ a F b
203 202 adantl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → if a = f d ⁡ c F b d ⁡ a F b = d ⁡ a F b
204 201 203 eqtr4d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = f d ⁡ c F b d ⁡ a F b
205 173 204 pm2.61dan ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = f d ⁡ c F b d ⁡ a F b
206 iffalse ⊢ ¬ a = c → if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b = if a = f d ⁡ c F b d ⁡ a F b
207 206 adantl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c → if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b = if a = f d ⁡ c F b d ⁡ a F b
208 205 207 eqtr4d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
209 153 208 pm2.61dan ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
210 209 3adant3 ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
211 210 mpoeq3dva ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → a ∈ N , b ∈ N ⟼ d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = a ∈ N , b ∈ N ⟼ if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
212 139 211 sylan ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → a ∈ N , b ∈ N ⟼ d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = a ∈ N , b ∈ N ⟼ if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
213 212 fveq2d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ if a = c d ⁡ f F b if a = f d ⁡ c F b d ⁡ a F b
214 fveq2 ⊢ a = c → d ⁡ a = d ⁡ c
215 214 oveq1d ⊢ a = c → d ⁡ a F b = d ⁡ c F b
216 iftrue ⊢ a = c → if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b = d ⁡ c F b
217 215 216 eqtr4d ⊢ a = c → d ⁡ a F b = if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
218 fveq2 ⊢ a = f → d ⁡ a = d ⁡ f
219 218 oveq1d ⊢ a = f → d ⁡ a F b = d ⁡ f F b
220 iftrue ⊢ a = f → if a = f d ⁡ f F b d ⁡ a F b = d ⁡ f F b
221 219 220 eqtr4d ⊢ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
222 221 adantl ⊢ ¬ a = c ∧ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
223 iffalse ⊢ ¬ a = f → if a = f d ⁡ f F b d ⁡ a F b = d ⁡ a F b
224 223 eqcomd ⊢ ¬ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
225 224 adantl ⊢ ¬ a = c ∧ ¬ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
226 222 225 pm2.61dan ⊢ ¬ a = c → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
227 iffalse ⊢ ¬ a = c → if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
228 226 227 eqtr4d ⊢ ¬ a = c → d ⁡ a F b = if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
229 217 228 pm2.61i ⊢ d ⁡ a F b = if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
230 229 a1i ⊢ a ∈ N ∧ b ∈ N → d ⁡ a F b = if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
231 230 mpoeq3ia ⊢ a ∈ N , b ∈ N ⟼ d ⁡ a F b = a ∈ N , b ∈ N ⟼ if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
232 231 fveq2i ⊢ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = D ⁡ a ∈ N , b ∈ N ⟼ if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
233 232 fveq2i ⊢ inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
234 233 a1i ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
235 138 213 234 3eqtr4d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
236 fveq1 ⊢ e = pmTrsp ⁡ N ⁡ c f → e ⁡ a = pmTrsp ⁡ N ⁡ c f ⁡ a
237 236 fveq2d ⊢ e = pmTrsp ⁡ N ⁡ c f → d ⁡ e ⁡ a = d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a
238 237 oveq1d ⊢ e = pmTrsp ⁡ N ⁡ c f → d ⁡ e ⁡ a F b = d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b
239 238 mpoeq3dv ⊢ e = pmTrsp ⁡ N ⁡ c f → a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = a ∈ N , b ∈ N ⟼ d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b
240 239 fveqeq2d ⊢ e = pmTrsp ⁡ N ⁡ c f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b ↔ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
241 235 240 syl5ibrcom ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → e = pmTrsp ⁡ N ⁡ c f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
242 241 expr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N → c ≠ f → e = pmTrsp ⁡ N ⁡ c f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
243 242 impd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N → c ≠ f ∧ e = pmTrsp ⁡ N ⁡ c f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
244 243 rexlimdvva ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N → ∃ c ∈ N ∃ f ∈ N c ≠ f ∧ e = pmTrsp ⁡ N ⁡ c f → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
245 113 244 syl5 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N → e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
246 245 3impia ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
247 111 246 syl3an2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
248 110 247 eqtrd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
249 248 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F → D ⁡ a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b = inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b
250 fveq2 ⊢ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F → inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F
251 250 adantl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F → inv g ⁡ R ⁡ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F
252 eqid ⊢ inv g ⁡ R = inv g ⁡ R
253 58 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → R ∈ Ring
254 65 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
255 254 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
256 66 3 mgpbas ⊢ K = Base mulGrp R
257 44 256 mhmf ⊢ ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R → ℤRHom ⁡ R ∘ pmSgn ⁡ N : Base SymGrp ⁡ N ⟶ K
258 255 257 syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N : Base SymGrp ⁡ N ⟶ K
259 258 93 ffvelcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d ∈ K
260 59 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D : B ⟶ K
261 simp13 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → F ∈ B
262 260 261 ffvelcdmd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ F ∈ K
263 3 7 252 253 259 262 ringmneg1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F = inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F
264 66 7 mgpplusg ⊢ · ˙ = + mulGrp R
265 44 43 264 mhmlin ⊢ ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ Base SymGrp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ e
266 255 93 95 265 syl3anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ e
267 45 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → N ∈ Fin
268 simp3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ ran ⁡ pmTrsp ⁡ N
269 46 44 50 pmtrodpm ⊢ N ∈ Fin ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ Base SymGrp ⁡ N ∖ pmEven ⁡ N
270 267 268 269 syl2anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ Base SymGrp ⁡ N ∖ pmEven ⁡ N
271 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
272 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
273 271 272 5 44 252 zrhpsgnodpm ⊢ R ∈ Ring ∧ N ∈ Fin ∧ e ∈ Base SymGrp ⁡ N ∖ pmEven ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ e = inv g ⁡ R ⁡ 1 ˙
274 253 267 270 273 syl3anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ e = inv g ⁡ R ⁡ 1 ˙
275 274 oveq2d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ e = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ inv g ⁡ R ⁡ 1 ˙
276 3 7 5 252 253 259 ringnegr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ inv g ⁡ R ⁡ 1 ˙ = inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d
277 266 275 276 3eqtrrd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e
278 277 oveq1d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e · ˙ D ⁡ F
279 263 278 eqtr3d ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e · ˙ D ⁡ F
280 279 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F → inv g ⁡ R ⁡ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e · ˙ D ⁡ F
281 249 251 280 3eqtrd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N ∧ D ⁡ a ∈ N , b ∈ N ⟼ d ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d · ˙ D ⁡ F → D ⁡ a ∈ N , b ∈ N ⟼ d + SymGrp ⁡ N e ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d + SymGrp ⁡ N e · ˙ D ⁡ F
282 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → E : N ⟶ 1-1 onto N
283 46 44 elsymgbas ⊢ N ∈ Fin → E ∈ Base SymGrp ⁡ N ↔ E : N ⟶ 1-1 onto N
284 45 283 syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → E ∈ Base SymGrp ⁡ N ↔ E : N ⟶ 1-1 onto N
285 282 284 mpbird ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → E ∈ Base SymGrp ⁡ N
286 20 27 34 41 42 43 44 49 52 57 92 281 285 mndind ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → D ⁡ a ∈ N , b ∈ N ⟼ E ⁡ a F b = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ E · ˙ D ⁡ F