Metamath Proof Explorer

Theorem mdetunilem2

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
mdetunilem2.ph ⊢ ψ → φ
mdetunilem2.eg ⊢ ψ → E ∈ N ∧ G ∈ N ∧ E ≠ G
mdetunilem2.f ⊢ ψ ∧ b ∈ N → F ∈ K
mdetunilem2.h ⊢ ψ ∧ a ∈ N ∧ b ∈ N → H ∈ K
Assertion mdetunilem2 ⊢ ψ → D ⁡ a ∈ N , b ∈ N ⟼ if a = E F if a = G F H = 0 ˙

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 mdetunilem2.ph ⊢ ψ → φ
15 mdetunilem2.eg ⊢ ψ → E ∈ N ∧ G ∈ N ∧ E ≠ G
16 mdetunilem2.f ⊢ ψ ∧ b ∈ N → F ∈ K
17 mdetunilem2.h ⊢ ψ ∧ a ∈ N ∧ b ∈ N → H ∈ K
18 14 8 syl ⊢ ψ → N ∈ Fin
19 14 9 syl ⊢ ψ → R ∈ Ring
20 16 3adant2 ⊢ ψ ∧ a ∈ N ∧ b ∈ N → F ∈ K
21 20 17 ifcld ⊢ ψ ∧ a ∈ N ∧ b ∈ N → if a = G F H ∈ K
22 20 21 ifcld ⊢ ψ ∧ a ∈ N ∧ b ∈ N → if a = E F if a = G F H ∈ K
23 1 3 2 18 19 22 matbas2d ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F if a = G F H ∈ B
24 eqidd ⊢ ψ ∧ w ∈ N → a ∈ N , b ∈ N ⟼ if a = E F if a = G F H = a ∈ N , b ∈ N ⟼ if a = E F if a = G F H
25 iftrue ⊢ a = E → if a = E F if a = G F H = F
26 csbeq1a ⊢ b = w → F = ⦋ w / b⦌ F
27 25 26 sylan9eq ⊢ a = E ∧ b = w → if a = E F if a = G F H = ⦋ w / b⦌ F
28 27 adantl ⊢ ψ ∧ w ∈ N ∧ a = E ∧ b = w → if a = E F if a = G F H = ⦋ w / b⦌ F
29 eqidd ⊢ ψ ∧ w ∈ N ∧ a = E → N = N
30 15 simp1d ⊢ ψ → E ∈ N
31 30 adantr ⊢ ψ ∧ w ∈ N → E ∈ N
32 simpr ⊢ ψ ∧ w ∈ N → w ∈ N
33 nfv ⊢ Ⅎ b ψ ∧ w ∈ N
34 nfcsb1v ⊢ Ⅎ _ b ⦋ w / b⦌ F
35 34 nfel1 ⊢ Ⅎ b ⦋ w / b⦌ F ∈ K
36 33 35 nfim ⊢ Ⅎ b ψ ∧ w ∈ N → ⦋ w / b⦌ F ∈ K
37 eleq1w ⊢ b = w → b ∈ N ↔ w ∈ N
38 37 anbi2d ⊢ b = w → ψ ∧ b ∈ N ↔ ψ ∧ w ∈ N
39 26 eleq1d ⊢ b = w → F ∈ K ↔ ⦋ w / b⦌ F ∈ K
40 38 39 imbi12d ⊢ b = w → ψ ∧ b ∈ N → F ∈ K ↔ ψ ∧ w ∈ N → ⦋ w / b⦌ F ∈ K
41 36 40 16 chvarfv ⊢ ψ ∧ w ∈ N → ⦋ w / b⦌ F ∈ K
42 nfv ⊢ Ⅎ a ψ ∧ w ∈ N
43 nfcv ⊢ Ⅎ _ b E
44 nfcv ⊢ Ⅎ _ a w
45 nfcv ⊢ Ⅎ _ a ⦋ w / b⦌ F
46 24 28 29 31 32 41 42 33 43 44 45 34 ovmpodxf ⊢ ψ ∧ w ∈ N → E a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w = ⦋ w / b⦌ F
47 15 simp3d ⊢ ψ → E ≠ G
48 47 adantr ⊢ ψ ∧ w ∈ N → E ≠ G
49 neeq2 ⊢ a = G → E ≠ a ↔ E ≠ G
50 48 49 syl5ibrcom ⊢ ψ ∧ w ∈ N → a = G → E ≠ a
51 50 imp ⊢ ψ ∧ w ∈ N ∧ a = G → E ≠ a
52 51 necomd ⊢ ψ ∧ w ∈ N ∧ a = G → a ≠ E
53 52 neneqd ⊢ ψ ∧ w ∈ N ∧ a = G → ¬ a = E
54 53 adantrr ⊢ ψ ∧ w ∈ N ∧ a = G ∧ b = w → ¬ a = E
55 54 iffalsed ⊢ ψ ∧ w ∈ N ∧ a = G ∧ b = w → if a = E F if a = G F H = if a = G F H
56 iftrue ⊢ a = G → if a = G F H = F
57 56 26 sylan9eq ⊢ a = G ∧ b = w → if a = G F H = ⦋ w / b⦌ F
58 57 adantl ⊢ ψ ∧ w ∈ N ∧ a = G ∧ b = w → if a = G F H = ⦋ w / b⦌ F
59 55 58 eqtrd ⊢ ψ ∧ w ∈ N ∧ a = G ∧ b = w → if a = E F if a = G F H = ⦋ w / b⦌ F
60 eqidd ⊢ ψ ∧ w ∈ N ∧ a = G → N = N
61 15 simp2d ⊢ ψ → G ∈ N
62 61 adantr ⊢ ψ ∧ w ∈ N → G ∈ N
63 nfcv ⊢ Ⅎ _ b G
64 24 59 60 62 32 41 42 33 63 44 45 34 ovmpodxf ⊢ ψ ∧ w ∈ N → G a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w = ⦋ w / b⦌ F
65 46 64 eqtr4d ⊢ ψ ∧ w ∈ N → E a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w = G a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w
66 65 ralrimiva ⊢ ψ → ∀ w ∈ N E a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w = G a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w
67 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem1 ⊢ φ ∧ a ∈ N , b ∈ N ⟼ if a = E F if a = G F H ∈ B ∧ ∀ w ∈ N E a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w = G a ∈ N , b ∈ N ⟼ if a = E F if a = G F H w ∧ E ∈ N ∧ G ∈ N ∧ E ≠ G → D ⁡ a ∈ N , b ∈ N ⟼ if a = E F if a = G F H = 0 ˙
68 14 23 66 15 67 syl31anc ⊢ ψ → D ⁡ a ∈ N , b ∈ N ⟼ if a = E F if a = G F H = 0 ˙