Metamath Proof Explorer

Theorem mdetunilem5

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

Ref Expression
Hypotheses mdetuni.a ⊢A=NMatR
mdetuni.b ⊢B=BaseA
mdetuni.k ⊢K=BaseR
mdetuni.0g ⊢0˙=0R
mdetuni.1r ⊢1˙=1R
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∈Ny≠z∧∀w∈Nyxw=zxw→D⁡x=0˙
mdetuni.li ⊢φ→∀x∈B∀y∈B∀z∈B∀w∈Nx↾w×N=y↾w×N+˙fz↾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∈Nx↾w×N=w×N×y·˙fz↾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⟼ifa=EF+˙GH=D⁡a∈N,b∈N⟼ifa=EFH+˙D⁡a∈N,b∈N⟼ifa=EGH

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢A=NMatR
2 mdetuni.b ⊢B=BaseA
3 mdetuni.k ⊢K=BaseR
4 mdetuni.0g ⊢0˙=0R
5 mdetuni.1r ⊢1˙=1R
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∈Ny≠z∧∀w∈Nyxw=zxw→D⁡x=0˙
12 mdetuni.li ⊢φ→∀x∈B∀y∈B∀z∈B∀w∈Nx↾w×N=y↾w×N+˙fz↾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∈Nx↾w×N=w×N×y·˙fz↾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→ifa=EF+˙GH∈K
26 1 3 2 17 18 25 matbas2d ⊢ψ→a∈N,b∈N⟼ifa=EF+˙GH∈B
27 20 24 ifcld ⊢ψ∧a∈N∧b∈N→ifa=EFH∈K
28 1 3 2 17 18 27 matbas2d ⊢ψ→a∈N,b∈N⟼ifa=EFH∈B
29 21 24 ifcld ⊢ψ∧a∈N∧b∈N→ifa=EGH∈K
30 1 3 2 17 18 29 matbas2d ⊢ψ→a∈N,b∈N⟼ifa=EGH∈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+˙fa∈E,b∈N⟼G=a∈E,b∈N⟼F+˙G
42 41 eqcomd ⊢ψ→a∈E,b∈N⟼F+˙G=a∈E,b∈N⟼F+˙fa∈E,b∈N⟼G
43 mposnif ⊢a∈E,b∈N⟼ifa=EF+˙GH=a∈E,b∈N⟼F+˙G
44 mposnif ⊢a∈E,b∈N⟼ifa=EFH=a∈E,b∈N⟼F
45 mposnif ⊢a∈E,b∈N⟼ifa=EGH=a∈E,b∈N⟼G
46 44 45 oveq12i ⊢a∈E,b∈N⟼ifa=EFH+˙fa∈E,b∈N⟼ifa=EGH=a∈E,b∈N⟼F+˙fa∈E,b∈N⟼G
47 42 43 46 3eqtr4g ⊢ψ→a∈E,b∈N⟼ifa=EF+˙GH=a∈E,b∈N⟼ifa=EFH+˙fa∈E,b∈N⟼ifa=EGH
48 ssid ⊢N⊆N
49 resmpo ⊢E⊆N∧N⊆N→a∈N,b∈N⟼ifa=EF+˙GH↾E×N=a∈E,b∈N⟼ifa=EF+˙GH
50 33 48 49 sylancl ⊢ψ→a∈N,b∈N⟼ifa=EF+˙GH↾E×N=a∈E,b∈N⟼ifa=EF+˙GH
51 resmpo ⊢E⊆N∧N⊆N→a∈N,b∈N⟼ifa=EFH↾E×N=a∈E,b∈N⟼ifa=EFH
52 33 48 51 sylancl ⊢ψ→a∈N,b∈N⟼ifa=EFH↾E×N=a∈E,b∈N⟼ifa=EFH
53 resmpo ⊢E⊆N∧N⊆N→a∈N,b∈N⟼ifa=EGH↾E×N=a∈E,b∈N⟼ifa=EGH
54 33 48 53 sylancl ⊢ψ→a∈N,b∈N⟼ifa=EGH↾E×N=a∈E,b∈N⟼ifa=EGH
55 52 54 oveq12d ⊢ψ→a∈N,b∈N⟼ifa=EFH↾E×N+˙fa∈N,b∈N⟼ifa=EGH↾E×N=a∈E,b∈N⟼ifa=EFH+˙fa∈E,b∈N⟼ifa=EGH
56 47 50 55 3eqtr4d ⊢ψ→a∈N,b∈N⟼ifa=EF+˙GH↾E×N=a∈N,b∈N⟼ifa=EFH↾E×N+˙fa∈N,b∈N⟼ifa=EGH↾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→ifa=EF+˙GH=H
61 iffalse ⊢¬a=E→ifa=EFH=H
62 60 61 eqtr4d ⊢¬a=E→ifa=EF+˙GH=ifa=EFH
63 59 62 syl ⊢ψ∧a∈N∖E∧b∈N→ifa=EF+˙GH=ifa=EFH
64 63 mpoeq3dva ⊢ψ→a∈N∖E,b∈N⟼ifa=EF+˙GH=a∈N∖E,b∈N⟼ifa=EFH
65 difss ⊢N∖E⊆N
66 resmpo ⊢N∖E⊆N∧N⊆N→a∈N,b∈N⟼ifa=EF+˙GH↾N∖E×N=a∈N∖E,b∈N⟼ifa=EF+˙GH
67 65 48 66 mp2an ⊢a∈N,b∈N⟼ifa=EF+˙GH↾N∖E×N=a∈N∖E,b∈N⟼ifa=EF+˙GH
68 resmpo ⊢N∖E⊆N∧N⊆N→a∈N,b∈N⟼ifa=EFH↾N∖E×N=a∈N∖E,b∈N⟼ifa=EFH
69 65 48 68 mp2an ⊢a∈N,b∈N⟼ifa=EFH↾N∖E×N=a∈N∖E,b∈N⟼ifa=EFH
70 64 67 69 3eqtr4g ⊢ψ→a∈N,b∈N⟼ifa=EF+˙GH↾N∖E×N=a∈N,b∈N⟼ifa=EFH↾N∖E×N
71 iffalse ⊢¬a=E→ifa=EGH=H
72 60 71 eqtr4d ⊢¬a=E→ifa=EF+˙GH=ifa=EGH
73 59 72 syl ⊢ψ∧a∈N∖E∧b∈N→ifa=EF+˙GH=ifa=EGH
74 73 mpoeq3dva ⊢ψ→a∈N∖E,b∈N⟼ifa=EF+˙GH=a∈N∖E,b∈N⟼ifa=EGH
75 resmpo ⊢N∖E⊆N∧N⊆N→a∈N,b∈N⟼ifa=EGH↾N∖E×N=a∈N∖E,b∈N⟼ifa=EGH
76 65 48 75 mp2an ⊢a∈N,b∈N⟼ifa=EGH↾N∖E×N=a∈N∖E,b∈N⟼ifa=EGH
77 74 67 76 3eqtr4g ⊢ψ→a∈N,b∈N⟼ifa=EF+˙GH↾N∖E×N=a∈N,b∈N⟼ifa=EGH↾N∖E×N
78 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem3 ⊢φ∧a∈N,b∈N⟼ifa=EF+˙GH∈B∧a∈N,b∈N⟼ifa=EFH∈B∧a∈N,b∈N⟼ifa=EGH∈B∧E∈N∧a∈N,b∈N⟼ifa=EF+˙GH↾E×N=a∈N,b∈N⟼ifa=EFH↾E×N+˙fa∈N,b∈N⟼ifa=EGH↾E×N∧a∈N,b∈N⟼ifa=EF+˙GH↾N∖E×N=a∈N,b∈N⟼ifa=EFH↾N∖E×N∧a∈N,b∈N⟼ifa=EF+˙GH↾N∖E×N=a∈N,b∈N⟼ifa=EGH↾N∖E×N→D⁡a∈N,b∈N⟼ifa=EF+˙GH=D⁡a∈N,b∈N⟼ifa=EFH+˙D⁡a∈N,b∈N⟼ifa=EGH
79 14 26 28 30 15 56 70 77 78 syl332anc ⊢ψ→D⁡a∈N,b∈N⟼ifa=EF+˙GH=D⁡a∈N,b∈N⟼ifa=EFH+˙D⁡a∈N,b∈N⟼ifa=EGH