MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetunilem2 Structured version   Visualization version   GIF version

Theorem mdetunilem2 20347
Description: Lemma for mdetuni 20356. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
mdetuni.a 𝐴 = (𝑁 Mat 𝑅)
mdetuni.b 𝐵 = (Base‘𝐴)
mdetuni.k 𝐾 = (Base‘𝑅)
mdetuni.0g 0 = (0g𝑅)
mdetuni.1r 1 = (1r𝑅)
mdetuni.pg + = (+g𝑅)
mdetuni.tg · = (.r𝑅)
mdetuni.n (𝜑𝑁 ∈ Fin)
mdetuni.r (𝜑𝑅 ∈ Ring)
mdetuni.ff (𝜑𝐷:𝐵𝐾)
mdetuni.al (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
mdetuni.li (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
mdetuni.sc (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
mdetunilem2.ph (𝜓𝜑)
mdetunilem2.eg (𝜓 → (𝐸𝑁𝐺𝑁𝐸𝐺))
mdetunilem2.f ((𝜓𝑏𝑁) → 𝐹𝐾)
mdetunilem2.h ((𝜓𝑎𝑁𝑏𝑁) → 𝐻𝐾)
Assertion
Ref Expression
mdetunilem2 (𝜓 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 )
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝐵,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝐾,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝑁,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥,𝐷,𝑦,𝑧,𝑤,𝑎,𝑏   𝑥, · ,𝑦,𝑧,𝑤   + ,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   0 ,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   1 ,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   𝑥,𝑅,𝑦,𝑧,𝑤   𝐴,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   𝑥,𝐸,𝑦,𝑧,𝑤   𝑥,𝐹,𝑦,𝑧,𝑤   𝑥,𝐺,𝑦,𝑧,𝑤   𝑥,𝐻,𝑦,𝑧,𝑤   𝜓,𝑎,𝑏,𝑥,𝑦,𝑧,𝑤   𝐸,𝑎,𝑏   𝐺,𝑎,𝑏   𝐹,𝑎
Allowed substitution hints:   𝑅(𝑎,𝑏)   · (𝑎,𝑏)   𝐹(𝑏)   𝐻(𝑎,𝑏)

Proof of Theorem mdetunilem2
StepHypRef Expression
1 mdetunilem2.ph . 2 (𝜓𝜑)
2 mdetuni.a . . 3 𝐴 = (𝑁 Mat 𝑅)
3 mdetuni.k . . 3 𝐾 = (Base‘𝑅)
4 mdetuni.b . . 3 𝐵 = (Base‘𝐴)
5 mdetuni.n . . . 4 (𝜑𝑁 ∈ Fin)
61, 5syl 17 . . 3 (𝜓𝑁 ∈ Fin)
7 mdetuni.r . . . 4 (𝜑𝑅 ∈ Ring)
81, 7syl 17 . . 3 (𝜓𝑅 ∈ Ring)
9 mdetunilem2.f . . . . 5 ((𝜓𝑏𝑁) → 𝐹𝐾)
1093adant2 1078 . . . 4 ((𝜓𝑎𝑁𝑏𝑁) → 𝐹𝐾)
11 mdetunilem2.h . . . . 5 ((𝜓𝑎𝑁𝑏𝑁) → 𝐻𝐾)
1210, 11ifcld 4108 . . . 4 ((𝜓𝑎𝑁𝑏𝑁) → if(𝑎 = 𝐺, 𝐹, 𝐻) ∈ 𝐾)
1310, 12ifcld 4108 . . 3 ((𝜓𝑎𝑁𝑏𝑁) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) ∈ 𝐾)
142, 3, 4, 6, 8, 13matbas2d 20157 . 2 (𝜓 → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))) ∈ 𝐵)
15 eqidd 2622 . . . . 5 ((𝜓𝑤𝑁) → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))))
16 iftrue 4069 . . . . . . 7 (𝑎 = 𝐸 → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = 𝐹)
17 csbeq1a 3527 . . . . . . 7 (𝑏 = 𝑤𝐹 = 𝑤 / 𝑏𝐹)
1816, 17sylan9eq 2675 . . . . . 6 ((𝑎 = 𝐸𝑏 = 𝑤) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = 𝑤 / 𝑏𝐹)
1918adantl 482 . . . . 5 (((𝜓𝑤𝑁) ∧ (𝑎 = 𝐸𝑏 = 𝑤)) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = 𝑤 / 𝑏𝐹)
20 eqidd 2622 . . . . 5 (((𝜓𝑤𝑁) ∧ 𝑎 = 𝐸) → 𝑁 = 𝑁)
21 mdetunilem2.eg . . . . . . 7 (𝜓 → (𝐸𝑁𝐺𝑁𝐸𝐺))
2221simp1d 1071 . . . . . 6 (𝜓𝐸𝑁)
2322adantr 481 . . . . 5 ((𝜓𝑤𝑁) → 𝐸𝑁)
24 simpr 477 . . . . 5 ((𝜓𝑤𝑁) → 𝑤𝑁)
25 nfv 1840 . . . . . . 7 𝑏(𝜓𝑤𝑁)
26 nfcsb1v 3534 . . . . . . . 8 𝑏𝑤 / 𝑏𝐹
2726nfel1 2775 . . . . . . 7 𝑏𝑤 / 𝑏𝐹𝐾
2825, 27nfim 1822 . . . . . 6 𝑏((𝜓𝑤𝑁) → 𝑤 / 𝑏𝐹𝐾)
29 eleq1 2686 . . . . . . . 8 (𝑏 = 𝑤 → (𝑏𝑁𝑤𝑁))
3029anbi2d 739 . . . . . . 7 (𝑏 = 𝑤 → ((𝜓𝑏𝑁) ↔ (𝜓𝑤𝑁)))
3117eleq1d 2683 . . . . . . 7 (𝑏 = 𝑤 → (𝐹𝐾𝑤 / 𝑏𝐹𝐾))
3230, 31imbi12d 334 . . . . . 6 (𝑏 = 𝑤 → (((𝜓𝑏𝑁) → 𝐹𝐾) ↔ ((𝜓𝑤𝑁) → 𝑤 / 𝑏𝐹𝐾)))
3328, 32, 9chvar 2261 . . . . 5 ((𝜓𝑤𝑁) → 𝑤 / 𝑏𝐹𝐾)
34 nfv 1840 . . . . 5 𝑎(𝜓𝑤𝑁)
35 nfcv 2761 . . . . 5 𝑏𝐸
36 nfcv 2761 . . . . 5 𝑎𝑤
37 nfcv 2761 . . . . 5 𝑎𝑤 / 𝑏𝐹
3815, 19, 20, 23, 24, 33, 34, 25, 35, 36, 37, 26ovmpt2dxf 6746 . . . 4 ((𝜓𝑤𝑁) → (𝐸(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = 𝑤 / 𝑏𝐹)
3921simp3d 1073 . . . . . . . . . . . . 13 (𝜓𝐸𝐺)
4039adantr 481 . . . . . . . . . . . 12 ((𝜓𝑤𝑁) → 𝐸𝐺)
41 neeq2 2853 . . . . . . . . . . . 12 (𝑎 = 𝐺 → (𝐸𝑎𝐸𝐺))
4240, 41syl5ibrcom 237 . . . . . . . . . . 11 ((𝜓𝑤𝑁) → (𝑎 = 𝐺𝐸𝑎))
4342imp 445 . . . . . . . . . 10 (((𝜓𝑤𝑁) ∧ 𝑎 = 𝐺) → 𝐸𝑎)
4443necomd 2845 . . . . . . . . 9 (((𝜓𝑤𝑁) ∧ 𝑎 = 𝐺) → 𝑎𝐸)
4544neneqd 2795 . . . . . . . 8 (((𝜓𝑤𝑁) ∧ 𝑎 = 𝐺) → ¬ 𝑎 = 𝐸)
4645adantrr 752 . . . . . . 7 (((𝜓𝑤𝑁) ∧ (𝑎 = 𝐺𝑏 = 𝑤)) → ¬ 𝑎 = 𝐸)
4746iffalsed 4074 . . . . . 6 (((𝜓𝑤𝑁) ∧ (𝑎 = 𝐺𝑏 = 𝑤)) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = if(𝑎 = 𝐺, 𝐹, 𝐻))
48 iftrue 4069 . . . . . . . 8 (𝑎 = 𝐺 → if(𝑎 = 𝐺, 𝐹, 𝐻) = 𝐹)
4948, 17sylan9eq 2675 . . . . . . 7 ((𝑎 = 𝐺𝑏 = 𝑤) → if(𝑎 = 𝐺, 𝐹, 𝐻) = 𝑤 / 𝑏𝐹)
5049adantl 482 . . . . . 6 (((𝜓𝑤𝑁) ∧ (𝑎 = 𝐺𝑏 = 𝑤)) → if(𝑎 = 𝐺, 𝐹, 𝐻) = 𝑤 / 𝑏𝐹)
5147, 50eqtrd 2655 . . . . 5 (((𝜓𝑤𝑁) ∧ (𝑎 = 𝐺𝑏 = 𝑤)) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = 𝑤 / 𝑏𝐹)
52 eqidd 2622 . . . . 5 (((𝜓𝑤𝑁) ∧ 𝑎 = 𝐺) → 𝑁 = 𝑁)
5321simp2d 1072 . . . . . 6 (𝜓𝐺𝑁)
5453adantr 481 . . . . 5 ((𝜓𝑤𝑁) → 𝐺𝑁)
55 nfcv 2761 . . . . 5 𝑏𝐺
5615, 51, 52, 54, 24, 33, 34, 25, 55, 36, 37, 26ovmpt2dxf 6746 . . . 4 ((𝜓𝑤𝑁) → (𝐺(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = 𝑤 / 𝑏𝐹)
5738, 56eqtr4d 2658 . . 3 ((𝜓𝑤𝑁) → (𝐸(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = (𝐺(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤))
5857ralrimiva 2961 . 2 (𝜓 → ∀𝑤𝑁 (𝐸(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = (𝐺(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤))
59 mdetuni.0g . . 3 0 = (0g𝑅)
60 mdetuni.1r . . 3 1 = (1r𝑅)
61 mdetuni.pg . . 3 + = (+g𝑅)
62 mdetuni.tg . . 3 · = (.r𝑅)
63 mdetuni.ff . . 3 (𝜑𝐷:𝐵𝐾)
64 mdetuni.al . . 3 (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
65 mdetuni.li . . 3 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
66 mdetuni.sc . . 3 (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
672, 4, 3, 59, 60, 61, 62, 5, 7, 63, 64, 65, 66mdetunilem1 20346 . 2 (((𝜑 ∧ (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))) ∈ 𝐵 ∧ ∀𝑤𝑁 (𝐸(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = (𝐺(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤)) ∧ (𝐸𝑁𝐺𝑁𝐸𝐺)) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 )
681, 14, 58, 21, 67syl31anc 1326 1 (𝜓 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  csb 3518  cdif 3556  ifcif 4063  {csn 4153   × cxp 5077  cres 5081  wf 5848  cfv 5852  (class class class)co 6610  cmpt2 6612  𝑓 cof 6855  Fincfn 7906  Basecbs 15788  +gcplusg 15869  .rcmulr 15870  0gc0g 16028  1rcur 18429  Ringcrg 18475   Mat cmat 20141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-ot 4162  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-sup 8299  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-fz 12276  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-sca 15885  df-vsca 15886  df-ip 15887  df-tset 15888  df-ple 15889  df-ds 15892  df-hom 15894  df-cco 15895  df-0g 16030  df-prds 16036  df-pws 16038  df-sra 19100  df-rgmod 19101  df-dsmm 20004  df-frlm 20019  df-mat 20142
This theorem is referenced by:  mdetunilem6  20351  mdetunilem8  20353
  Copyright terms: Public domain W3C validator