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 ffvelrnd ⊢ φ ∧ 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 biimpri ⊢ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N ∧ f ∈ N ∧ c ≠ f
117 116 adantl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N ∧ f ∈ N ∧ c ≠ f
118 84 85 syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → F : N × N ⟶ K
119 118 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N → F : N × N ⟶ K
120 119 ad2antrr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → F : N × N ⟶ K
121 simpllr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d : N ⟶ N
122 simprlr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → f ∈ N
123 122 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → f ∈ N
124 121 123 ffvelrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ f ∈ N
125 simpr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → b ∈ N
126 120 124 125 fovrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ f F b ∈ K
127 simprll ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N
128 127 adantr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → c ∈ N
129 121 128 ffvelrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ c ∈ N
130 120 129 125 fovrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ b ∈ N → d ⁡ c F b ∈ K
131 126 130 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
132 118 ad2antrr ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → F : N × N ⟶ K
133 132 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
134 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
135 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → a ∈ N
136 134 135 ffvelrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → d ⁡ a ∈ N
137 simp3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ b ∈ N → b ∈ N
138 133 136 137 fovrnd ⊢ φ ∧ 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
139 1 2 3 4 5 6 7 8 9 10 11 12 13 114 117 131 138 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
140 simpl1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d : N ⟶ N → φ
141 fveq2 ⊢ a = c → pmTrsp ⁡ N ⁡ c f ⁡ a = pmTrsp ⁡ N ⁡ c f ⁡ c
142 8 adantr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → N ∈ Fin
143 simprll ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ∈ N
144 simprlr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → f ∈ N
145 simprr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → c ≠ f
146 112 pmtrprfv ⊢ N ∈ Fin ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → pmTrsp ⁡ N ⁡ c f ⁡ c = f
147 142 143 144 145 146 syl13anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f → pmTrsp ⁡ N ⁡ c f ⁡ c = f
148 147 adantr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ c = f
149 141 148 sylan9eqr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → pmTrsp ⁡ N ⁡ c f ⁡ a = f
150 149 fveq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a = d ⁡ f
151 150 oveq1d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = c → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = d ⁡ f F b
152 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
153 152 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
154 151 153 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
155 fveq2 ⊢ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = pmTrsp ⁡ N ⁡ c f ⁡ f
156 prcom ⊢ c f = f c
157 156 fveq2i ⊢ pmTrsp ⁡ N ⁡ c f = pmTrsp ⁡ N ⁡ f c
158 157 fveq1i ⊢ pmTrsp ⁡ N ⁡ c f ⁡ f = pmTrsp ⁡ N ⁡ f c ⁡ f
159 8 ad2antrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → N ∈ Fin
160 simplrl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c ∈ N ∧ f ∈ N
161 160 simprd ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → f ∈ N
162 160 simpld ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c ∈ N
163 simplrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c ≠ f
164 163 necomd ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → f ≠ c
165 112 pmtrprfv ⊢ N ∈ Fin ∧ f ∈ N ∧ c ∈ N ∧ f ≠ c → pmTrsp ⁡ N ⁡ f c ⁡ f = c
166 159 161 162 164 165 syl13anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ f c ⁡ f = c
167 158 166 syl5eq ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ f = c
168 155 167 sylan9eqr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = c
169 168 fveq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a = d ⁡ c
170 169 oveq1d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b = d ⁡ c F b
171 iftrue ⊢ a = f → if a = f d ⁡ c F b d ⁡ a F b = d ⁡ c F b
172 171 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
173 170 172 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
174 173 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
175 vex ⊢ a ∈ V
176 175 elpr ⊢ a ∈ c f ↔ a = c ∨ a = f
177 176 notbii ⊢ ¬ a ∈ c f ↔ ¬ a = c ∨ a = f
178 ioran ⊢ ¬ a = c ∨ a = f ↔ ¬ a = c ∧ ¬ a = f
179 177 178 sylbbr ⊢ ¬ a = c ∧ ¬ a = f → ¬ a ∈ c f
180 179 adantll ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → ¬ a ∈ c f
181 prssi ⊢ c ∈ N ∧ f ∈ N → c f ⊆ N
182 160 181 syl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c f ⊆ N
183 pr2ne ⊢ c ∈ N ∧ f ∈ N → c f ≈ 2 𝑜 ↔ c ≠ f
184 160 183 syl ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c f ≈ 2 𝑜 ↔ c ≠ f
185 163 184 mpbird ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → c f ≈ 2 𝑜
186 112 pmtrmvd ⊢ N ∈ Fin ∧ c f ⊆ N ∧ c f ≈ 2 𝑜 → dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I = c f
187 159 182 185 186 syl3anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I = c f
188 187 eleq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ a ∈ c f
189 188 notbid ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ ¬ a ∈ c f
190 189 ad2antrr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ ¬ a ∈ c f
191 180 190 mpbird ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
192 112 pmtrf ⊢ N ∈ Fin ∧ c f ⊆ N ∧ c f ≈ 2 𝑜 → pmTrsp ⁡ N ⁡ c f : N ⟶ N
193 159 182 185 192 syl3anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f : N ⟶ N
194 193 ffnd ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f Fn N
195 simpr ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → a ∈ N
196 fnelnfp ⊢ pmTrsp ⁡ N ⁡ c f Fn N ∧ a ∈ N → a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I ↔ pmTrsp ⁡ N ⁡ c f ⁡ a ≠ a
197 196 necon2bbid ⊢ pmTrsp ⁡ N ⁡ c f Fn N ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ a = a ↔ ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
198 194 195 197 syl2anc ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N → pmTrsp ⁡ N ⁡ c f ⁡ a = a ↔ ¬ a ∈ dom ⁡ pmTrsp ⁡ N ⁡ c f ∖ I
199 198 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
200 191 199 mpbird ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → pmTrsp ⁡ N ⁡ c f ⁡ a = a
201 200 fveq2d ⊢ φ ∧ c ∈ N ∧ f ∈ N ∧ c ≠ f ∧ a ∈ N ∧ ¬ a = c ∧ ¬ a = f → d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a = d ⁡ a
202 201 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
203 iffalse ⊢ ¬ a = f → if a = f d ⁡ c F b d ⁡ a F b = d ⁡ a F b
204 203 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
205 202 204 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
206 174 205 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
207 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
208 207 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
209 206 208 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
210 154 209 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
211 210 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
212 211 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
213 140 212 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
214 213 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
215 fveq2 ⊢ a = c → d ⁡ a = d ⁡ c
216 215 oveq1d ⊢ a = c → d ⁡ a F b = d ⁡ c F b
217 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
218 216 217 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
219 fveq2 ⊢ a = f → d ⁡ a = d ⁡ f
220 219 oveq1d ⊢ a = f → d ⁡ a F b = d ⁡ f F b
221 iftrue ⊢ a = f → if a = f d ⁡ f F b d ⁡ a F b = d ⁡ f F b
222 220 221 eqtr4d ⊢ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
223 222 adantl ⊢ ¬ a = c ∧ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
224 iffalse ⊢ ¬ a = f → if a = f d ⁡ f F b d ⁡ a F b = d ⁡ a F b
225 224 eqcomd ⊢ ¬ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
226 225 adantl ⊢ ¬ a = c ∧ ¬ a = f → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
227 223 226 pm2.61dan ⊢ ¬ a = c → d ⁡ a F b = if a = f d ⁡ f F b d ⁡ a F b
228 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
229 227 228 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
230 218 229 pm2.61i ⊢ d ⁡ a F b = if a = c d ⁡ c F b if a = f d ⁡ f F b d ⁡ a F b
231 230 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
232 231 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
233 232 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
234 233 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
235 234 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
236 139 214 235 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
237 fveq1 ⊢ e = pmTrsp ⁡ N ⁡ c f → e ⁡ a = pmTrsp ⁡ N ⁡ c f ⁡ a
238 237 fveq2d ⊢ e = pmTrsp ⁡ N ⁡ c f → d ⁡ e ⁡ a = d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a
239 238 oveq1d ⊢ e = pmTrsp ⁡ N ⁡ c f → d ⁡ e ⁡ a F b = d ⁡ pmTrsp ⁡ N ⁡ c f ⁡ a F b
240 239 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
241 240 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
242 236 241 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
243 242 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
244 243 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
245 244 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
246 113 245 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
247 246 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
248 111 247 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
249 110 248 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
250 249 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
251 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
252 251 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
253 eqid ⊢ inv g ⁡ R = inv g ⁡ R
254 58 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → R ∈ Ring
255 65 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
256 255 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
257 66 3 mgpbas ⊢ K = Base mulGrp R
258 44 257 mhmf ⊢ ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R → ℤRHom ⁡ R ∘ pmSgn ⁡ N : Base SymGrp ⁡ N ⟶ K
259 256 258 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
260 259 93 ffvelrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ d ∈ K
261 59 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D : B ⟶ K
262 simp13 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → F ∈ B
263 261 262 ffvelrnd ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → D ⁡ F ∈ K
264 3 7 253 254 260 263 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
265 66 7 mgpplusg ⊢ · ˙ = + mulGrp R
266 44 43 265 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
267 256 93 95 266 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
268 45 3ad2ant1 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → N ∈ Fin
269 simp3 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ ran ⁡ pmTrsp ⁡ N
270 46 44 50 pmtrodpm ⊢ N ∈ Fin ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ Base SymGrp ⁡ N ∖ pmEven ⁡ N
271 268 269 270 syl2anc ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B ∧ d ∈ Base SymGrp ⁡ N ∧ e ∈ ran ⁡ pmTrsp ⁡ N → e ∈ Base SymGrp ⁡ N ∖ pmEven ⁡ N
272 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
273 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
274 272 273 5 44 253 zrhpsgnodpm ⊢ R ∈ Ring ∧ N ∈ Fin ∧ e ∈ Base SymGrp ⁡ N ∖ pmEven ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ e = inv g ⁡ R ⁡ 1 ˙
275 254 268 271 274 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 ˙
276 275 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 ˙
277 3 7 5 253 254 260 rngnegr ⊢ φ ∧ 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
278 267 276 277 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
279 278 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
280 264 279 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
281 280 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
282 250 252 281 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
283 simp2 ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → E : N ⟶ 1-1 onto N
284 46 44 elsymgbas ⊢ N ∈ Fin → E ∈ Base SymGrp ⁡ N ↔ E : N ⟶ 1-1 onto N
285 45 284 syl ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → E ∈ Base SymGrp ⁡ N ↔ E : N ⟶ 1-1 onto N
286 283 285 mpbird ⊢ φ ∧ E : N ⟶ 1-1 onto N ∧ F ∈ B → E ∈ Base SymGrp ⁡ N
287 20 27 34 41 42 43 44 49 52 57 92 282 286 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