Metamath Proof Explorer


Theorem mdetunilem4

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

Ref Expression
Hypotheses 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 mdetunilem4 ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ( ๐ป โˆˆ ๐‘ โˆง ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) )

Proof

Step Hyp Ref Expression
1 mdetuni.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 mdetuni.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 mdetuni.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
4 mdetuni.0g โŠข 0 = ( 0g โ€˜ ๐‘… )
5 mdetuni.1r โŠข 1 = ( 1r โ€˜ ๐‘… )
6 mdetuni.pg โŠข + = ( +g โ€˜ ๐‘… )
7 mdetuni.tg โŠข ยท = ( .r โ€˜ ๐‘… )
8 mdetuni.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ Fin )
9 mdetuni.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
10 mdetuni.ff โŠข ( ๐œ‘ โ†’ ๐ท : ๐ต โŸถ ๐พ )
11 mdetuni.al โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐‘ โˆ€ ๐‘ง โˆˆ ๐‘ ( ( ๐‘ฆ โ‰  ๐‘ง โˆง โˆ€ ๐‘ค โˆˆ ๐‘ ( ๐‘ฆ ๐‘ฅ ๐‘ค ) = ( ๐‘ง ๐‘ฅ ๐‘ค ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = 0 ) )
12 mdetuni.li โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ๐‘ฆ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) โˆ˜f + ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ฆ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = ( ( ๐ท โ€˜ ๐‘ฆ ) + ( ๐ท โ€˜ ๐‘ง ) ) ) )
13 mdetuni.sc โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐พ โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) )
14 simp32 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ( ๐ป โˆˆ ๐‘ โˆง ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) ) โ†’ ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) )
15 simp33 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ( ๐ป โˆˆ ๐‘ โˆง ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) ) โ†’ ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) )
16 simp1 โŠข ( ( ๐ป โˆˆ ๐‘ โˆง ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) โ†’ ๐ป โˆˆ ๐‘ )
17 simp23 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ ๐บ โˆˆ ๐ต )
18 simp3 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ ๐ป โˆˆ ๐‘ )
19 simp21 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ ๐ธ โˆˆ ๐ต )
20 simp22 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ ๐น โˆˆ ๐พ )
21 13 3ad2ant1 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐พ โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) )
22 reseq1 โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) )
23 22 eqeq1d โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โ†” ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) ) )
24 reseq1 โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) )
25 24 eqeq1d โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) โ†” ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) )
26 23 25 anbi12d โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†” ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) ) )
27 fveqeq2 โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ( ๐ท โ€˜ ๐‘ฅ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) โ†” ( ๐ท โ€˜ ๐ธ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) )
28 26 27 imbi12d โŠข ( ๐‘ฅ = ๐ธ โ†’ ( ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) โ†” ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) ) )
29 28 2ralbidv โŠข ( ๐‘ฅ = ๐ธ โ†’ ( โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) โ†” โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) ) )
30 sneq โŠข ( ๐‘ฆ = ๐น โ†’ { ๐‘ฆ } = { ๐น } )
31 30 xpeq2d โŠข ( ๐‘ฆ = ๐น โ†’ ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) = ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) )
32 31 oveq1d โŠข ( ๐‘ฆ = ๐น โ†’ ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) )
33 32 eqeq2d โŠข ( ๐‘ฆ = ๐น โ†’ ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โ†” ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) ) )
34 33 anbi1d โŠข ( ๐‘ฆ = ๐น โ†’ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†” ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) ) )
35 oveq1 โŠข ( ๐‘ฆ = ๐น โ†’ ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) )
36 35 eqeq2d โŠข ( ๐‘ฆ = ๐น โ†’ ( ( ๐ท โ€˜ ๐ธ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) โ†” ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) )
37 34 36 imbi12d โŠข ( ๐‘ฆ = ๐น โ†’ ( ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) โ†” ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) ) )
38 37 2ralbidv โŠข ( ๐‘ฆ = ๐น โ†’ ( โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) โ†” โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) ) )
39 29 38 rspc2va โŠข ( ( ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐พ โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐‘ฅ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐‘ฆ } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐‘ฅ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐‘ฅ ) = ( ๐‘ฆ ยท ( ๐ท โ€˜ ๐‘ง ) ) ) ) โ†’ โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) )
40 19 20 21 39 syl21anc โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) )
41 reseq1 โŠข ( ๐‘ง = ๐บ โ†’ ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) )
42 41 oveq2d โŠข ( ๐‘ง = ๐บ โ†’ ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) )
43 42 eqeq2d โŠข ( ๐‘ง = ๐บ โ†’ ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โ†” ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) ) )
44 reseq1 โŠข ( ๐‘ง = ๐บ โ†’ ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) )
45 44 eqeq2d โŠข ( ๐‘ง = ๐บ โ†’ ( ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) โ†” ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) )
46 43 45 anbi12d โŠข ( ๐‘ง = ๐บ โ†’ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†” ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) ) )
47 fveq2 โŠข ( ๐‘ง = ๐บ โ†’ ( ๐ท โ€˜ ๐‘ง ) = ( ๐ท โ€˜ ๐บ ) )
48 47 oveq2d โŠข ( ๐‘ง = ๐บ โ†’ ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) )
49 48 eqeq2d โŠข ( ๐‘ง = ๐บ โ†’ ( ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) โ†” ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) )
50 46 49 imbi12d โŠข ( ๐‘ง = ๐บ โ†’ ( ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) โ†” ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) ) )
51 sneq โŠข ( ๐‘ค = ๐ป โ†’ { ๐‘ค } = { ๐ป } )
52 51 xpeq1d โŠข ( ๐‘ค = ๐ป โ†’ ( { ๐‘ค } ร— ๐‘ ) = ( { ๐ป } ร— ๐‘ ) )
53 52 reseq2d โŠข ( ๐‘ค = ๐ป โ†’ ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) )
54 52 xpeq1d โŠข ( ๐‘ค = ๐ป โ†’ ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) = ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) )
55 52 reseq2d โŠข ( ๐‘ค = ๐ป โ†’ ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) )
56 54 55 oveq12d โŠข ( ๐‘ค = ๐ป โ†’ ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) )
57 53 56 eqeq12d โŠข ( ๐‘ค = ๐ป โ†’ ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โ†” ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) ) )
58 51 difeq2d โŠข ( ๐‘ค = ๐ป โ†’ ( ๐‘ โˆ– { ๐‘ค } ) = ( ๐‘ โˆ– { ๐ป } ) )
59 58 xpeq1d โŠข ( ๐‘ค = ๐ป โ†’ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) = ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) )
60 59 reseq2d โŠข ( ๐‘ค = ๐ป โ†’ ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) )
61 59 reseq2d โŠข ( ๐‘ค = ๐ป โ†’ ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) )
62 60 61 eqeq12d โŠข ( ๐‘ค = ๐ป โ†’ ( ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) โ†” ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) )
63 57 62 anbi12d โŠข ( ๐‘ค = ๐ป โ†’ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†” ( ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) ) )
64 63 imbi1d โŠข ( ๐‘ค = ๐ป โ†’ ( ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) โ†” ( ( ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) ) )
65 50 64 rspc2va โŠข ( ( ( ๐บ โˆˆ ๐ต โˆง ๐ป โˆˆ ๐‘ ) โˆง โˆ€ ๐‘ง โˆˆ ๐ต โˆ€ ๐‘ค โˆˆ ๐‘ ( ( ( ๐ธ โ†พ ( { ๐‘ค } ร— ๐‘ ) ) = ( ( ( { ๐‘ค } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐‘ง โ†พ ( { ๐‘ค } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) = ( ๐‘ง โ†พ ( ( ๐‘ โˆ– { ๐‘ค } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐‘ง ) ) ) ) โ†’ ( ( ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) )
66 17 18 40 65 syl21anc โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ๐ป โˆˆ ๐‘ ) โ†’ ( ( ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) )
67 16 66 syl3an3 โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ( ๐ป โˆˆ ๐‘ โˆง ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) ) โ†’ ( ( ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) ) )
68 14 15 67 mp2and โŠข ( ( ๐œ‘ โˆง ( ๐ธ โˆˆ ๐ต โˆง ๐น โˆˆ ๐พ โˆง ๐บ โˆˆ ๐ต ) โˆง ( ๐ป โˆˆ ๐‘ โˆง ( ๐ธ โ†พ ( { ๐ป } ร— ๐‘ ) ) = ( ( ( { ๐ป } ร— ๐‘ ) ร— { ๐น } ) โˆ˜f ยท ( ๐บ โ†พ ( { ๐ป } ร— ๐‘ ) ) ) โˆง ( ๐ธ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) = ( ๐บ โ†พ ( ( ๐‘ โˆ– { ๐ป } ) ร— ๐‘ ) ) ) ) โ†’ ( ๐ท โ€˜ ๐ธ ) = ( ๐น ยท ( ๐ท โ€˜ ๐บ ) ) )