Metamath Proof Explorer

Theorem mdetunilem5

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
mdetunilem5.ph ⊢ ψ → φ
mdetunilem5.e ⊢ ψ → E ∈ N
mdetunilem5.fgh ⊢ ψ ∧ a ∈ N ∧ b ∈ N → F ∈ K ∧ G ∈ K ∧ H ∈ K
Assertion mdetunilem5 ⊢ ψ → D ⁡ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H = D ⁡ a ∈ N , b ∈ N ⟼ if a = E F H + ˙ D ⁡ a ∈ N , b ∈ N ⟼ if a = E G H

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 mdetunilem5.ph ⊢ ψ → φ
15 mdetunilem5.e ⊢ ψ → E ∈ N
16 mdetunilem5.fgh ⊢ ψ ∧ a ∈ N ∧ b ∈ N → F ∈ K ∧ G ∈ K ∧ H ∈ K
17 14 8 syl ⊢ ψ → N ∈ Fin
18 14 9 syl ⊢ ψ → R ∈ Ring
19 18 3ad2ant1 ⊢ ψ ∧ a ∈ N ∧ b ∈ N → R ∈ Ring
20 16 simp1d ⊢ ψ ∧ a ∈ N ∧ b ∈ N → F ∈ K
21 16 simp2d ⊢ ψ ∧ a ∈ N ∧ b ∈ N → G ∈ K
22 3 6 ringacl ⊢ R ∈ Ring ∧ F ∈ K ∧ G ∈ K → F + ˙ G ∈ K
23 19 20 21 22 syl3anc ⊢ ψ ∧ a ∈ N ∧ b ∈ N → F + ˙ G ∈ K
24 16 simp3d ⊢ ψ ∧ a ∈ N ∧ b ∈ N → H ∈ K
25 23 24 ifcld ⊢ ψ ∧ a ∈ N ∧ b ∈ N → if a = E F + ˙ G H ∈ K
26 1 3 2 17 18 25 matbas2d ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ∈ B
27 20 24 ifcld ⊢ ψ ∧ a ∈ N ∧ b ∈ N → if a = E F H ∈ K
28 1 3 2 17 18 27 matbas2d ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F H ∈ B
29 21 24 ifcld ⊢ ψ ∧ a ∈ N ∧ b ∈ N → if a = E G H ∈ K
30 1 3 2 17 18 29 matbas2d ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E G H ∈ B
31 snex ⊢ E ∈ V
32 31 a1i ⊢ ψ → E ∈ V
33 15 snssd ⊢ ψ → E ⊆ N
34 33 3ad2ant1 ⊢ ψ ∧ a ∈ E ∧ b ∈ N → E ⊆ N
35 simp2 ⊢ ψ ∧ a ∈ E ∧ b ∈ N → a ∈ E
36 34 35 sseldd ⊢ ψ ∧ a ∈ E ∧ b ∈ N → a ∈ N
37 36 20 syld3an2 ⊢ ψ ∧ a ∈ E ∧ b ∈ N → F ∈ K
38 36 21 syld3an2 ⊢ ψ ∧ a ∈ E ∧ b ∈ N → G ∈ K
39 eqidd ⊢ ψ → a ∈ E , b ∈ N ⟼ F = a ∈ E , b ∈ N ⟼ F
40 eqidd ⊢ ψ → a ∈ E , b ∈ N ⟼ G = a ∈ E , b ∈ N ⟼ G
41 32 17 37 38 39 40 offval22 ⊢ ψ → a ∈ E , b ∈ N ⟼ F + ˙ f a ∈ E , b ∈ N ⟼ G = a ∈ E , b ∈ N ⟼ F + ˙ G
42 41 eqcomd ⊢ ψ → a ∈ E , b ∈ N ⟼ F + ˙ G = a ∈ E , b ∈ N ⟼ F + ˙ f a ∈ E , b ∈ N ⟼ G
43 mposnif ⊢ a ∈ E , b ∈ N ⟼ if a = E F + ˙ G H = a ∈ E , b ∈ N ⟼ F + ˙ G
44 mposnif ⊢ a ∈ E , b ∈ N ⟼ if a = E F H = a ∈ E , b ∈ N ⟼ F
45 mposnif ⊢ a ∈ E , b ∈ N ⟼ if a = E G H = a ∈ E , b ∈ N ⟼ G
46 44 45 oveq12i ⊢ a ∈ E , b ∈ N ⟼ if a = E F H + ˙ f a ∈ E , b ∈ N ⟼ if a = E G H = a ∈ E , b ∈ N ⟼ F + ˙ f a ∈ E , b ∈ N ⟼ G
47 42 43 46 3eqtr4g ⊢ ψ → a ∈ E , b ∈ N ⟼ if a = E F + ˙ G H = a ∈ E , b ∈ N ⟼ if a = E F H + ˙ f a ∈ E , b ∈ N ⟼ if a = E G H
48 ssid ⊢ N ⊆ N
49 resmpo ⊢ E ⊆ N ∧ N ⊆ N → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E F + ˙ G H
50 33 48 49 sylancl ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E F + ˙ G H
51 resmpo ⊢ E ⊆ N ∧ N ⊆ N → a ∈ N , b ∈ N ⟼ if a = E F H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E F H
52 33 48 51 sylancl ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E F H
53 resmpo ⊢ E ⊆ N ∧ N ⊆ N → a ∈ N , b ∈ N ⟼ if a = E G H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E G H
54 33 48 53 sylancl ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E G H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E G H
55 52 54 oveq12d ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F H ↾ E × N + ˙ f a ∈ N , b ∈ N ⟼ if a = E G H ↾ E × N = a ∈ E , b ∈ N ⟼ if a = E F H + ˙ f a ∈ E , b ∈ N ⟼ if a = E G H
56 47 50 55 3eqtr4d ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ E × N = a ∈ N , b ∈ N ⟼ if a = E F H ↾ E × N + ˙ f a ∈ N , b ∈ N ⟼ if a = E G H ↾ E × N
57 eldifsni ⊢ a ∈ N ∖ E → a ≠ E
58 57 3ad2ant2 ⊢ ψ ∧ a ∈ N ∖ E ∧ b ∈ N → a ≠ E
59 58 neneqd ⊢ ψ ∧ a ∈ N ∖ E ∧ b ∈ N → ¬ a = E
60 iffalse ⊢ ¬ a = E → if a = E F + ˙ G H = H
61 iffalse ⊢ ¬ a = E → if a = E F H = H
62 60 61 eqtr4d ⊢ ¬ a = E → if a = E F + ˙ G H = if a = E F H
63 59 62 syl ⊢ ψ ∧ a ∈ N ∖ E ∧ b ∈ N → if a = E F + ˙ G H = if a = E F H
64 63 mpoeq3dva ⊢ ψ → a ∈ N ∖ E , b ∈ N ⟼ if a = E F + ˙ G H = a ∈ N ∖ E , b ∈ N ⟼ if a = E F H
65 difss ⊢ N ∖ E ⊆ N
66 resmpo ⊢ N ∖ E ⊆ N ∧ N ⊆ N → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ N ∖ E × N = a ∈ N ∖ E , b ∈ N ⟼ if a = E F + ˙ G H
67 65 48 66 mp2an ⊢ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ N ∖ E × N = a ∈ N ∖ E , b ∈ N ⟼ if a = E F + ˙ G H
68 resmpo ⊢ N ∖ E ⊆ N ∧ N ⊆ N → a ∈ N , b ∈ N ⟼ if a = E F H ↾ N ∖ E × N = a ∈ N ∖ E , b ∈ N ⟼ if a = E F H
69 65 48 68 mp2an ⊢ a ∈ N , b ∈ N ⟼ if a = E F H ↾ N ∖ E × N = a ∈ N ∖ E , b ∈ N ⟼ if a = E F H
70 64 67 69 3eqtr4g ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ N ∖ E × N = a ∈ N , b ∈ N ⟼ if a = E F H ↾ N ∖ E × N
71 iffalse ⊢ ¬ a = E → if a = E G H = H
72 60 71 eqtr4d ⊢ ¬ a = E → if a = E F + ˙ G H = if a = E G H
73 59 72 syl ⊢ ψ ∧ a ∈ N ∖ E ∧ b ∈ N → if a = E F + ˙ G H = if a = E G H
74 73 mpoeq3dva ⊢ ψ → a ∈ N ∖ E , b ∈ N ⟼ if a = E F + ˙ G H = a ∈ N ∖ E , b ∈ N ⟼ if a = E G H
75 resmpo ⊢ N ∖ E ⊆ N ∧ N ⊆ N → a ∈ N , b ∈ N ⟼ if a = E G H ↾ N ∖ E × N = a ∈ N ∖ E , b ∈ N ⟼ if a = E G H
76 65 48 75 mp2an ⊢ a ∈ N , b ∈ N ⟼ if a = E G H ↾ N ∖ E × N = a ∈ N ∖ E , b ∈ N ⟼ if a = E G H
77 74 67 76 3eqtr4g ⊢ ψ → a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ N ∖ E × N = a ∈ N , b ∈ N ⟼ if a = E G H ↾ N ∖ E × N
78 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem3 ⊢ φ ∧ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ∈ B ∧ a ∈ N , b ∈ N ⟼ if a = E F H ∈ B ∧ a ∈ N , b ∈ N ⟼ if a = E G H ∈ B ∧ E ∈ N ∧ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ E × N = a ∈ N , b ∈ N ⟼ if a = E F H ↾ E × N + ˙ f a ∈ N , b ∈ N ⟼ if a = E G H ↾ E × N ∧ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ N ∖ E × N = a ∈ N , b ∈ N ⟼ if a = E F H ↾ N ∖ E × N ∧ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H ↾ N ∖ E × N = a ∈ N , b ∈ N ⟼ if a = E G H ↾ N ∖ E × N → D ⁡ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H = D ⁡ a ∈ N , b ∈ N ⟼ if a = E F H + ˙ D ⁡ a ∈ N , b ∈ N ⟼ if a = E G H
79 14 26 28 30 15 56 70 77 78 syl332anc ⊢ ψ → D ⁡ a ∈ N , b ∈ N ⟼ if a = E F + ˙ G H = D ⁡ a ∈ N , b ∈ N ⟼ if a = E F H + ˙ D ⁡ a ∈ N , b ∈ N ⟼ if a = E G H