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

Theorem mdetunilem1 21984
Description: Lemma for mdetuni 21994. (Contributed by SO, 14-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 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))))
mdetuni.sc (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐พ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((({๐‘ค} ร— ๐‘) ร— {๐‘ฆ}) โˆ˜f ยท (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = (๐‘ฆ ยท (๐ทโ€˜๐‘ง))))
Assertion
Ref Expression
mdetunilem1 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ (๐ทโ€˜๐ธ) = 0 )
Distinct variable groups:   ๐œ‘,๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐ต,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐พ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐‘,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐ท,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ, ยท ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ, + ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ, 0 ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ, 1 ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐‘…,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐ด,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐ธ,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐น,๐‘ฆ,๐‘ง,๐‘ค   ๐‘ฅ,๐บ,๐‘ฆ,๐‘ง,๐‘ค

Proof of Theorem mdetunilem1
StepHypRef Expression
1 simpr3 1197 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ ๐น โ‰  ๐บ)
2 simpl3 1194 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค))
3 neeq2 3004 . . . . 5 (๐‘ง = ๐บ โ†’ (๐น โ‰  ๐‘ง โ†” ๐น โ‰  ๐บ))
4 oveq1 7368 . . . . . . 7 (๐‘ง = ๐บ โ†’ (๐‘ง๐ธ๐‘ค) = (๐บ๐ธ๐‘ค))
54eqeq2d 2744 . . . . . 6 (๐‘ง = ๐บ โ†’ ((๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค) โ†” (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)))
65ralbidv 3171 . . . . 5 (๐‘ง = ๐บ โ†’ (โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค) โ†” โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)))
73, 6anbi12d 632 . . . 4 (๐‘ง = ๐บ โ†’ ((๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†” (๐น โ‰  ๐บ โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค))))
87imbi1d 342 . . 3 (๐‘ง = ๐บ โ†’ (((๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 ) โ†” ((๐น โ‰  ๐บ โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 )))
9 simpl2 1193 . . . 4 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ ๐ธ โˆˆ ๐ต)
10 simpr1 1195 . . . 4 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ ๐น โˆˆ ๐‘)
11 simpl1 1192 . . . . 5 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ ๐œ‘)
12 mdetuni.al . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค)) โ†’ (๐ทโ€˜๐‘ฅ) = 0 ))
1311, 12syl 17 . . . 4 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค)) โ†’ (๐ทโ€˜๐‘ฅ) = 0 ))
14 oveq 7367 . . . . . . . . . 10 (๐‘ฅ = ๐ธ โ†’ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ฆ๐ธ๐‘ค))
15 oveq 7367 . . . . . . . . . 10 (๐‘ฅ = ๐ธ โ†’ (๐‘ง๐‘ฅ๐‘ค) = (๐‘ง๐ธ๐‘ค))
1614, 15eqeq12d 2749 . . . . . . . . 9 (๐‘ฅ = ๐ธ โ†’ ((๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค) โ†” (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)))
1716ralbidv 3171 . . . . . . . 8 (๐‘ฅ = ๐ธ โ†’ (โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค) โ†” โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)))
1817anbi2d 630 . . . . . . 7 (๐‘ฅ = ๐ธ โ†’ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค)) โ†” (๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค))))
19 fveqeq2 6855 . . . . . . 7 (๐‘ฅ = ๐ธ โ†’ ((๐ทโ€˜๐‘ฅ) = 0 โ†” (๐ทโ€˜๐ธ) = 0 ))
2018, 19imbi12d 345 . . . . . 6 (๐‘ฅ = ๐ธ โ†’ (((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค)) โ†’ (๐ทโ€˜๐‘ฅ) = 0 ) โ†” ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 )))
2120ralbidv 3171 . . . . 5 (๐‘ฅ = ๐ธ โ†’ (โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค)) โ†’ (๐ทโ€˜๐‘ฅ) = 0 ) โ†” โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 )))
22 neeq1 3003 . . . . . . . 8 (๐‘ฆ = ๐น โ†’ (๐‘ฆ โ‰  ๐‘ง โ†” ๐น โ‰  ๐‘ง))
23 oveq1 7368 . . . . . . . . . 10 (๐‘ฆ = ๐น โ†’ (๐‘ฆ๐ธ๐‘ค) = (๐น๐ธ๐‘ค))
2423eqeq1d 2735 . . . . . . . . 9 (๐‘ฆ = ๐น โ†’ ((๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค) โ†” (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)))
2524ralbidv 3171 . . . . . . . 8 (๐‘ฆ = ๐น โ†’ (โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค) โ†” โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)))
2622, 25anbi12d 632 . . . . . . 7 (๐‘ฆ = ๐น โ†’ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†” (๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค))))
2726imbi1d 342 . . . . . 6 (๐‘ฆ = ๐น โ†’ (((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 ) โ†” ((๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 )))
2827ralbidv 3171 . . . . 5 (๐‘ฆ = ๐น โ†’ (โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 ) โ†” โˆ€๐‘ง โˆˆ ๐‘ ((๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 )))
2921, 28rspc2va 3593 . . . 4 (((๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฆ โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐‘ฆ๐‘ฅ๐‘ค) = (๐‘ง๐‘ฅ๐‘ค)) โ†’ (๐ทโ€˜๐‘ฅ) = 0 )) โ†’ โˆ€๐‘ง โˆˆ ๐‘ ((๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 ))
309, 10, 13, 29syl21anc 837 . . 3 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ โˆ€๐‘ง โˆˆ ๐‘ ((๐น โ‰  ๐‘ง โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐‘ง๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 ))
31 simpr2 1196 . . 3 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ ๐บ โˆˆ ๐‘)
328, 30, 31rspcdva 3584 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ ((๐น โ‰  ๐บ โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โ†’ (๐ทโ€˜๐ธ) = 0 ))
331, 2, 32mp2and 698 1 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง โˆ€๐‘ค โˆˆ ๐‘ (๐น๐ธ๐‘ค) = (๐บ๐ธ๐‘ค)) โˆง (๐น โˆˆ ๐‘ โˆง ๐บ โˆˆ ๐‘ โˆง ๐น โ‰  ๐บ)) โ†’ (๐ทโ€˜๐ธ) = 0 )
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061   โˆ– cdif 3911  {csn 4590   ร— cxp 5635   โ†พ cres 5639  โŸถwf 6496  โ€˜cfv 6500  (class class class)co 7361   โˆ˜f cof 7619  Fincfn 8889  Basecbs 17091  +gcplusg 17141  .rcmulr 17142  0gc0g 17329  1rcur 19921  Ringcrg 19972   Mat cmat 21777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-ov 7364
This theorem is referenced by:  mdetunilem2  21985  mdetuni0  21993
  Copyright terms: Public domain W3C validator