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

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

Proof of Theorem mdetunilem3
StepHypRef Expression
1 simp23 1209 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ โˆง (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘)))) โˆง ((๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))) โ†’ (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))))
2 simp3l 1202 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ โˆง (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘)))) โˆง ((๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))) โ†’ (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))
3 simp3r 1203 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ โˆง (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘)))) โˆง ((๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))) โ†’ (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))
4 simprl 770 . . . . 5 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ ๐บ โˆˆ ๐ต)
5 simprr 772 . . . . 5 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ ๐ป โˆˆ ๐‘)
6 simpl2 1193 . . . . . 6 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ ๐ธ โˆˆ ๐ต)
7 simpl3 1194 . . . . . 6 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ ๐น โˆˆ ๐ต)
8 simpl1 1192 . . . . . . 7 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ ๐œ‘)
9 mdetuni.li . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))))
108, 9syl 17 . . . . . 6 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))))
11 reseq1 5935 . . . . . . . . . . 11 (๐‘ฅ = ๐ธ โ†’ (๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = (๐ธ โ†พ ({๐‘ค} ร— ๐‘)))
1211eqeq1d 2735 . . . . . . . . . 10 (๐‘ฅ = ๐ธ โ†’ ((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โ†” (๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘)))))
13 reseq1 5935 . . . . . . . . . . 11 (๐‘ฅ = ๐ธ โ†’ (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)))
1413eqeq1d 2735 . . . . . . . . . 10 (๐‘ฅ = ๐ธ โ†’ ((๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โ†” (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))))
1513eqeq1d 2735 . . . . . . . . . 10 (๐‘ฅ = ๐ธ โ†’ ((๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โ†” (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))))
1612, 14, 153anbi123d 1437 . . . . . . . . 9 (๐‘ฅ = ๐ธ โ†’ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†” ((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)))))
17 fveq2 6846 . . . . . . . . . 10 (๐‘ฅ = ๐ธ โ†’ (๐ทโ€˜๐‘ฅ) = (๐ทโ€˜๐ธ))
1817eqeq1d 2735 . . . . . . . . 9 (๐‘ฅ = ๐ธ โ†’ ((๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง)) โ†” (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))))
1916, 18imbi12d 345 . . . . . . . 8 (๐‘ฅ = ๐ธ โ†’ ((((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))) โ†” (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง)))))
20192ralbidv 3209 . . . . . . 7 (๐‘ฅ = ๐ธ โ†’ (โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))) โ†” โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง)))))
21 reseq1 5935 . . . . . . . . . . . 12 (๐‘ฆ = ๐น โ†’ (๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) = (๐น โ†พ ({๐‘ค} ร— ๐‘)))
2221oveq1d 7376 . . . . . . . . . . 11 (๐‘ฆ = ๐น โ†’ ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))))
2322eqeq2d 2744 . . . . . . . . . 10 (๐‘ฆ = ๐น โ†’ ((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โ†” (๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘)))))
24 reseq1 5935 . . . . . . . . . . 11 (๐‘ฆ = ๐น โ†’ (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)))
2524eqeq2d 2744 . . . . . . . . . 10 (๐‘ฆ = ๐น โ†’ ((๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โ†” (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))))
2623, 253anbi12d 1438 . . . . . . . . 9 (๐‘ฆ = ๐น โ†’ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†” ((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)))))
27 fveq2 6846 . . . . . . . . . . 11 (๐‘ฆ = ๐น โ†’ (๐ทโ€˜๐‘ฆ) = (๐ทโ€˜๐น))
2827oveq1d 7376 . . . . . . . . . 10 (๐‘ฆ = ๐น โ†’ ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง)) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง)))
2928eqeq2d 2744 . . . . . . . . 9 (๐‘ฆ = ๐น โ†’ ((๐ทโ€˜๐ธ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง)) โ†” (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง))))
3026, 29imbi12d 345 . . . . . . . 8 (๐‘ฆ = ๐น โ†’ ((((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))) โ†” (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง)))))
31302ralbidv 3209 . . . . . . 7 (๐‘ฆ = ๐น โ†’ (โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง))) โ†” โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง)))))
3220, 31rspc2va 3593 . . . . . 6 (((๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐‘ฅ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐‘ฆ โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ฆ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐‘ฅ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐‘ฅ) = ((๐ทโ€˜๐‘ฆ) + (๐ทโ€˜๐‘ง)))) โ†’ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง))))
336, 7, 10, 32syl21anc 837 . . . . 5 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง))))
34 reseq1 5935 . . . . . . . . . 10 (๐‘ง = ๐บ โ†’ (๐‘ง โ†พ ({๐‘ค} ร— ๐‘)) = (๐บ โ†พ ({๐‘ค} ร— ๐‘)))
3534oveq2d 7377 . . . . . . . . 9 (๐‘ง = ๐บ โ†’ ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))))
3635eqeq2d 2744 . . . . . . . 8 (๐‘ง = ๐บ โ†’ ((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โ†” (๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘)))))
37 reseq1 5935 . . . . . . . . 9 (๐‘ง = ๐บ โ†’ (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)))
3837eqeq2d 2744 . . . . . . . 8 (๐‘ง = ๐บ โ†’ ((๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โ†” (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))))
3936, 383anbi13d 1439 . . . . . . 7 (๐‘ง = ๐บ โ†’ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†” ((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)))))
40 fveq2 6846 . . . . . . . . 9 (๐‘ง = ๐บ โ†’ (๐ทโ€˜๐‘ง) = (๐ทโ€˜๐บ))
4140oveq2d 7377 . . . . . . . 8 (๐‘ง = ๐บ โ†’ ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง)) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ)))
4241eqeq2d 2744 . . . . . . 7 (๐‘ง = ๐บ โ†’ ((๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง)) โ†” (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ))))
4339, 42imbi12d 345 . . . . . 6 (๐‘ง = ๐บ โ†’ ((((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง))) โ†” (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ)))))
44 sneq 4600 . . . . . . . . . . 11 (๐‘ค = ๐ป โ†’ {๐‘ค} = {๐ป})
4544xpeq1d 5666 . . . . . . . . . 10 (๐‘ค = ๐ป โ†’ ({๐‘ค} ร— ๐‘) = ({๐ป} ร— ๐‘))
4645reseq2d 5941 . . . . . . . . 9 (๐‘ค = ๐ป โ†’ (๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = (๐ธ โ†พ ({๐ป} ร— ๐‘)))
4745reseq2d 5941 . . . . . . . . . 10 (๐‘ค = ๐ป โ†’ (๐น โ†พ ({๐‘ค} ร— ๐‘)) = (๐น โ†พ ({๐ป} ร— ๐‘)))
4845reseq2d 5941 . . . . . . . . . 10 (๐‘ค = ๐ป โ†’ (๐บ โ†พ ({๐‘ค} ร— ๐‘)) = (๐บ โ†พ ({๐ป} ร— ๐‘)))
4947, 48oveq12d 7379 . . . . . . . . 9 (๐‘ค = ๐ป โ†’ ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))))
5046, 49eqeq12d 2749 . . . . . . . 8 (๐‘ค = ๐ป โ†’ ((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))) โ†” (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘)))))
5144difeq2d 4086 . . . . . . . . . . 11 (๐‘ค = ๐ป โ†’ (๐‘ โˆ– {๐‘ค}) = (๐‘ โˆ– {๐ป}))
5251xpeq1d 5666 . . . . . . . . . 10 (๐‘ค = ๐ป โ†’ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘) = ((๐‘ โˆ– {๐ป}) ร— ๐‘))
5352reseq2d 5941 . . . . . . . . 9 (๐‘ค = ๐ป โ†’ (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))
5452reseq2d 5941 . . . . . . . . 9 (๐‘ค = ๐ป โ†’ (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))
5553, 54eqeq12d 2749 . . . . . . . 8 (๐‘ค = ๐ป โ†’ ((๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โ†” (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))))
5652reseq2d 5941 . . . . . . . . 9 (๐‘ค = ๐ป โ†’ (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))
5753, 56eqeq12d 2749 . . . . . . . 8 (๐‘ค = ๐ป โ†’ ((๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โ†” (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))))
5850, 55, 573anbi123d 1437 . . . . . . 7 (๐‘ค = ๐ป โ†’ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†” ((๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))))
5958imbi1d 342 . . . . . 6 (๐‘ค = ๐ป โ†’ ((((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ))) โ†” (((๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ)))))
6043, 59rspc2va 3593 . . . . 5 (((๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘) โˆง โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐‘ (((๐ธ โ†พ ({๐‘ค} ร— ๐‘)) = ((๐น โ†พ ({๐‘ค} ร— ๐‘)) โˆ˜f + (๐‘ง โ†พ ({๐‘ค} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘)) = (๐‘ง โ†พ ((๐‘ โˆ– {๐‘ค}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐‘ง)))) โ†’ (((๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ))))
614, 5, 33, 60syl21anc 837 . . . 4 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘)) โ†’ (((๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ))))
62613adantr3 1172 . . 3 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ โˆง (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))))) โ†’ (((๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ))))
63623adant3 1133 . 2 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ โˆง (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘)))) โˆง ((๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))) โ†’ (((๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘))) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ))))
641, 2, 3, 63mp3and 1465 1 (((๐œ‘ โˆง ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐ต) โˆง (๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ โˆง (๐ธ โ†พ ({๐ป} ร— ๐‘)) = ((๐น โ†พ ({๐ป} ร— ๐‘)) โˆ˜f + (๐บ โ†พ ({๐ป} ร— ๐‘)))) โˆง ((๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐น โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) โˆง (๐ธ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)) = (๐บ โ†พ ((๐‘ โˆ– {๐ป}) ร— ๐‘)))) โ†’ (๐ทโ€˜๐ธ) = ((๐ทโ€˜๐น) + (๐ทโ€˜๐บ)))
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-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-opab 5172  df-xp 5643  df-res 5649  df-iota 6452  df-fv 6508  df-ov 7364
This theorem is referenced by:  mdetunilem5  21988  mdetuni0  21993
  Copyright terms: Public domain W3C validator