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

Theorem madugsum 22455
Description: The determinant of a matrix with a row ๐ฟ consisting of the same element ๐‘‹ is the sum of the elements of the ๐ฟ-th column of the adjunct of the matrix multiplied with ๐‘‹. (Contributed by Stefan O'Rear, 16-Jul-2018.)
Hypotheses
Ref Expression
maduf.a ๐ด = (๐‘ Mat ๐‘…)
maduf.j ๐ฝ = (๐‘ maAdju ๐‘…)
maduf.b ๐ต = (Baseโ€˜๐ด)
madugsum.d ๐ท = (๐‘ maDet ๐‘…)
madugsum.t ยท = (.rโ€˜๐‘…)
madugsum.k ๐พ = (Baseโ€˜๐‘…)
madugsum.m (๐œ‘ โ†’ ๐‘€ โˆˆ ๐ต)
madugsum.r (๐œ‘ โ†’ ๐‘… โˆˆ CRing)
madugsum.x ((๐œ‘ โˆง ๐‘– โˆˆ ๐‘) โ†’ ๐‘‹ โˆˆ ๐พ)
madugsum.l (๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘)
Assertion
Ref Expression
madugsum (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)))))
Distinct variable groups:   ๐‘–,๐‘,๐‘—   ๐‘…,๐‘–,๐‘—   ๐ต,๐‘–,๐‘—   ๐œ‘,๐‘–,๐‘—   ๐‘–,๐ฝ   ๐‘–,๐พ,๐‘—   ๐‘–,๐‘€,๐‘—   ๐‘—,๐‘‹   ยท ,๐‘–   ๐‘–,๐ฟ,๐‘—
Allowed substitution hints:   ๐ด(๐‘–,๐‘—)   ๐ท(๐‘–,๐‘—)   ยท (๐‘—)   ๐ฝ(๐‘—)   ๐‘‹(๐‘–)

Proof of Theorem madugsum
Dummy variables ๐‘Ž ๐‘ ๐‘ ๐‘‘ ๐‘’ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpteq1 5231 . . . . 5 (๐‘ = โˆ… โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
21oveq2d 7417 . . . 4 (๐‘ = โˆ… โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
3 eleq2 2814 . . . . . . . 8 (๐‘ = โˆ… โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ โˆ…))
43ifbid 4543 . . . . . . 7 (๐‘ = โˆ… โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
54ifeq1d 4539 . . . . . 6 (๐‘ = โˆ… โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
65mpoeq3dv 7480 . . . . 5 (๐‘ = โˆ… โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
76fveq2d 6885 . . . 4 (๐‘ = โˆ… โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
82, 7eqeq12d 2740 . . 3 (๐‘ = โˆ… โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
9 mpteq1 5231 . . . . 5 (๐‘ = ๐‘‘ โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
109oveq2d 7417 . . . 4 (๐‘ = ๐‘‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
11 eleq2 2814 . . . . . . . 8 (๐‘ = ๐‘‘ โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ ๐‘‘))
1211ifbid 4543 . . . . . . 7 (๐‘ = ๐‘‘ โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
1312ifeq1d 4539 . . . . . 6 (๐‘ = ๐‘‘ โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
1413mpoeq3dv 7480 . . . . 5 (๐‘ = ๐‘‘ โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
1514fveq2d 6885 . . . 4 (๐‘ = ๐‘‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
1610, 15eqeq12d 2740 . . 3 (๐‘ = ๐‘‘ โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
17 mpteq1 5231 . . . . 5 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
1817oveq2d 7417 . . . 4 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
19 eleq2 2814 . . . . . . . 8 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ (๐‘‘ โˆช {๐‘’})))
2019ifbid 4543 . . . . . . 7 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
2120ifeq1d 4539 . . . . . 6 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
2221mpoeq3dv 7480 . . . . 5 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
2322fveq2d 6885 . . . 4 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
2418, 23eqeq12d 2740 . . 3 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
25 mpteq1 5231 . . . . 5 (๐‘ = ๐‘ โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
2625oveq2d 7417 . . . 4 (๐‘ = ๐‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
27 eleq2 2814 . . . . . . . 8 (๐‘ = ๐‘ โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ ๐‘))
2827ifbid 4543 . . . . . . 7 (๐‘ = ๐‘ โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
2928ifeq1d 4539 . . . . . 6 (๐‘ = ๐‘ โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
3029mpoeq3dv 7480 . . . . 5 (๐‘ = ๐‘ โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
3130fveq2d 6885 . . . 4 (๐‘ = ๐‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
3226, 31eqeq12d 2740 . . 3 (๐‘ = ๐‘ โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
33 mpt0 6682 . . . . . 6 (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = โˆ…
3433oveq2i 7412 . . . . 5 (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg โˆ…)
35 eqid 2724 . . . . . 6 (0gโ€˜๐‘…) = (0gโ€˜๐‘…)
3635gsum0 18604 . . . . 5 (๐‘… ฮฃg โˆ…) = (0gโ€˜๐‘…)
3734, 36eqtri 2752 . . . 4 (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (0gโ€˜๐‘…)
38 noel 4322 . . . . . . . . 9 ยฌ ๐‘ โˆˆ โˆ…
39 iffalse 4529 . . . . . . . . 9 (ยฌ ๐‘ โˆˆ โˆ… โ†’ if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
4038, 39mp1i 13 . . . . . . . 8 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
4140ifeq1d 4539 . . . . . . 7 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘)))
4241mpoeq3ia 7479 . . . . . 6 (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘)))
4342fveq2i 6884 . . . . 5 (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘))))
44 madugsum.d . . . . . 6 ๐ท = (๐‘ maDet ๐‘…)
45 madugsum.k . . . . . 6 ๐พ = (Baseโ€˜๐‘…)
46 madugsum.r . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ CRing)
47 madugsum.m . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐ต)
48 maduf.a . . . . . . . . 9 ๐ด = (๐‘ Mat ๐‘…)
49 maduf.b . . . . . . . . 9 ๐ต = (Baseโ€˜๐ด)
5048, 49matrcl 22222 . . . . . . . 8 (๐‘€ โˆˆ ๐ต โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
5147, 50syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
5251simpld 494 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ Fin)
5348, 45, 49matbas2i 22234 . . . . . . . . 9 (๐‘€ โˆˆ ๐ต โ†’ ๐‘€ โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)))
54 elmapi 8838 . . . . . . . . 9 (๐‘€ โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ๐พ)
5547, 53, 543syl 18 . . . . . . . 8 (๐œ‘ โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ๐พ)
5655fovcdmda 7571 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘)) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
57563impb 1112 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
58 madugsum.l . . . . . 6 (๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘)
5944, 45, 35, 46, 52, 57, 58mdetr0 22417 . . . . 5 (๐œ‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘)))) = (0gโ€˜๐‘…))
6043, 59eqtrid 2776 . . . 4 (๐œ‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (0gโ€˜๐‘…))
6137, 60eqtr4id 2783 . . 3 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
62 eqid 2724 . . . . . . 7 (+gโ€˜๐‘…) = (+gโ€˜๐‘…)
6346adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ CRing)
64 crngring 20135 . . . . . . . . 9 (๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring)
6563, 64syl 17 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ Ring)
66 ringcmn 20166 . . . . . . . 8 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd)
6765, 66syl 17 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ CMnd)
6852adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘ โˆˆ Fin)
69 simprl 768 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘‘ โІ ๐‘)
7068, 69ssfid 9262 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘‘ โˆˆ Fin)
7165adantr 480 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ ๐‘… โˆˆ Ring)
7269sselda 3974 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ ๐‘ โˆˆ ๐‘)
73 madugsum.x . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘– โˆˆ ๐‘) โ†’ ๐‘‹ โˆˆ ๐พ)
7473ralrimiva 3138 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
7574ad2antrr 723 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
76 rspcsbela 4427 . . . . . . . . 9 ((๐‘ โˆˆ ๐‘ โˆง โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
7772, 75, 76syl2anc 583 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
78 maduf.j . . . . . . . . . . . . . 14 ๐ฝ = (๐‘ maAdju ๐‘…)
7948, 78, 49maduf 22453 . . . . . . . . . . . . 13 (๐‘… โˆˆ CRing โ†’ ๐ฝ:๐ตโŸถ๐ต)
8046, 79syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ:๐ตโŸถ๐ต)
8180, 47ffvelcdmd 7077 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฝโ€˜๐‘€) โˆˆ ๐ต)
8248, 45, 49matbas2i 22234 . . . . . . . . . . 11 ((๐ฝโ€˜๐‘€) โˆˆ ๐ต โ†’ (๐ฝโ€˜๐‘€) โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)))
83 elmapi 8838 . . . . . . . . . . 11 ((๐ฝโ€˜๐‘€) โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)) โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
8481, 82, 833syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
8584ad2antrr 723 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
8658ad2antrr 723 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ ๐ฟ โˆˆ ๐‘)
8785, 72, 86fovcdmd 7572 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ (๐‘(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ)
88 madugsum.t . . . . . . . . 9 ยท = (.rโ€˜๐‘…)
8945, 88ringcl 20140 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง (๐‘(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ) โ†’ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
9071, 77, 87, 89syl3anc 1368 . . . . . . 7 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
91 vex 3470 . . . . . . . 8 ๐‘’ โˆˆ V
9291a1i 11 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘’ โˆˆ V)
93 eldifn 4119 . . . . . . . 8 (๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘) โ†’ ยฌ ๐‘’ โˆˆ ๐‘‘)
9493ad2antll 726 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ยฌ ๐‘’ โˆˆ ๐‘‘)
95 eldifi 4118 . . . . . . . . . 10 (๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘) โ†’ ๐‘’ โˆˆ ๐‘)
9695ad2antll 726 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘’ โˆˆ ๐‘)
9774adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
98 rspcsbela 4427 . . . . . . . . 9 ((๐‘’ โˆˆ ๐‘ โˆง โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ) โ†’ โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
9996, 97, 98syl2anc 583 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
10084adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
10158adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐ฟ โˆˆ ๐‘)
102100, 96, 101fovcdmd 7572 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ)
10345, 88ringcl 20140 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
10465, 99, 102, 103syl3anc 1368 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
105 csbeq1 3888 . . . . . . . 8 (๐‘ = ๐‘’ โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
106 oveq1 7408 . . . . . . . 8 (๐‘ = ๐‘’ โ†’ (๐‘(๐ฝโ€˜๐‘€)๐ฟ) = (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))
107105, 106oveq12d 7419 . . . . . . 7 (๐‘ = ๐‘’ โ†’ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)))
10845, 62, 67, 70, 90, 92, 94, 104, 107gsumunsn 19865 . . . . . 6 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
109108adantr 480 . . . . 5 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
110 oveq1 7408 . . . . . 6 ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
111110adantl 481 . . . . 5 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
112 elun 4140 . . . . . . . . . . . . . 14 (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ โˆˆ {๐‘’}))
113 velsn 4636 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ {๐‘’} โ†” ๐‘ = ๐‘’)
114113orbi2i 909 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ โˆˆ {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’))
115112, 114bitri 275 . . . . . . . . . . . . 13 (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’))
116 ifbi 4542 . . . . . . . . . . . . 13 ((๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’)) โ†’ if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
117115, 116ax-mp 5 . . . . . . . . . . . 12 if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))
118 ringmnd 20133 . . . . . . . . . . . . . . 15 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd)
11965, 118syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ Mnd)
1201193ad2ant1 1130 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘… โˆˆ Mnd)
121 simp3 1135 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ ๐‘)
122973ad2ant1 1130 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
123121, 122, 76syl2anc 583 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
124 elequ1 2105 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘’ โ†’ (๐‘ โˆˆ ๐‘‘ โ†” ๐‘’ โˆˆ ๐‘‘))
125124biimpac 478 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’) โ†’ ๐‘’ โˆˆ ๐‘‘)
12694, 125nsyl 140 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ยฌ (๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’))
1271263ad2ant1 1130 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ยฌ (๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’))
12845, 35, 62mndifsplit 22448 . . . . . . . . . . . . 13 ((๐‘… โˆˆ Mnd โˆง โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง ยฌ (๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’)) โ†’ if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))))
129120, 123, 127, 128syl3anc 1368 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))))
130117, 129eqtrid 2776 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))))
131105adantl 481 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ = ๐‘’) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
132131ifeq1da 4551 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ = ๐‘’, โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
133 ovif2 7499 . . . . . . . . . . . . . . 15 (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) = if(๐‘ = ๐‘’, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)), (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…)))
134 eqid 2724 . . . . . . . . . . . . . . . . . 18 (1rโ€˜๐‘…) = (1rโ€˜๐‘…)
13545, 88, 134ringridm 20154 . . . . . . . . . . . . . . . . 17 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)) = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
13665, 99, 135syl2anc 583 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)) = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
13745, 88, 35ringrz 20178 . . . . . . . . . . . . . . . . 17 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
13865, 99, 137syl2anc 583 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
139136, 138ifeq12d 4541 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)), (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…))) = if(๐‘ = ๐‘’, โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
140133, 139eqtrid 2776 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) = if(๐‘ = ๐‘’, โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
141132, 140eqtr4d 2767 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))))
142141oveq2d 7417 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))))
1431423ad2ant1 1130 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))))
144130, 143eqtrd 2764 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))))
145144ifeq1d 4539 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘)))
146145mpoeq3dva 7478 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘))))
147146fveq2d 6885 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘)))))
14845, 35ring0cl 20151 . . . . . . . . . . 11 (๐‘… โˆˆ Ring โ†’ (0gโ€˜๐‘…) โˆˆ ๐พ)
14965, 148syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (0gโ€˜๐‘…) โˆˆ ๐พ)
1501493ad2ant1 1130 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (0gโ€˜๐‘…) โˆˆ ๐พ)
151123, 150ifcld 4566 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) โˆˆ ๐พ)
15245, 134ringidcl 20150 . . . . . . . . . . . 12 (๐‘… โˆˆ Ring โ†’ (1rโ€˜๐‘…) โˆˆ ๐พ)
15365, 152syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (1rโ€˜๐‘…) โˆˆ ๐พ)
154153, 149ifcld 4566 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)) โˆˆ ๐พ)
15545, 88ringcl 20140 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)) โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) โˆˆ ๐พ)
15665, 99, 154, 155syl3anc 1368 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) โˆˆ ๐พ)
1571563ad2ant1 1130 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) โˆˆ ๐พ)
15855adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ๐พ)
159158fovcdmda 7571 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘)) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
1601593impb 1112 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
16144, 45, 62, 63, 68, 151, 157, 160, 101mdetrlin2 22419 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘)))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘))))))
1621543ad2ant1 1130 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)) โˆˆ ๐พ)
16344, 45, 88, 63, 68, 162, 160, 99, 101mdetrsca2 22416 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘)))) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
16447adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘€ โˆˆ ๐ต)
16548, 44, 78, 49, 134, 35maducoeval 22451 . . . . . . . . . . 11 ((๐‘€ โˆˆ ๐ต โˆง ๐‘’ โˆˆ ๐‘ โˆง ๐ฟ โˆˆ ๐‘) โ†’ (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
166164, 96, 101, 165syl3anc 1368 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
167166oveq2d 7417 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
168163, 167eqtr4d 2767 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘)))) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)))
169168oveq2d 7417 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘))))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
170147, 161, 1693eqtrrd 2769 . . . . . 6 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
171170adantr 480 . . . . 5 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
172109, 111, 1713eqtrd 2768 . . . 4 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
173172ex 412 . . 3 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
1748, 16, 24, 32, 61, 173, 52findcard2d 9161 . 2 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
175 nfcv 2895 . . . 4 โ„ฒ๐‘(๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ))
176 nfcsb1v 3910 . . . . 5 โ„ฒ๐‘–โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹
177 nfcv 2895 . . . . 5 โ„ฒ๐‘– ยท
178 nfcv 2895 . . . . 5 โ„ฒ๐‘–(๐‘(๐ฝโ€˜๐‘€)๐ฟ)
179176, 177, 178nfov 7431 . . . 4 โ„ฒ๐‘–(โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))
180 csbeq1a 3899 . . . . 5 (๐‘– = ๐‘ โ†’ ๐‘‹ = โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹)
181 oveq1 7408 . . . . 5 (๐‘– = ๐‘ โ†’ (๐‘–(๐ฝโ€˜๐‘€)๐ฟ) = (๐‘(๐ฝโ€˜๐‘€)๐ฟ))
182180, 181oveq12d 7419 . . . 4 (๐‘– = ๐‘ โ†’ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)) = (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))
183175, 179, 182cbvmpt 5249 . . 3 (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))
184183oveq2i 7412 . 2 (๐‘… ฮฃg (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
185 nfcv 2895 . . . . 5 โ„ฒ๐‘Žif(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))
186 nfcv 2895 . . . . 5 โ„ฒ๐‘if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))
187 nfcv 2895 . . . . 5 โ„ฒ๐‘—if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘))
188 nfv 1909 . . . . . 6 โ„ฒ๐‘– ๐‘Ž = ๐ฟ
189 nfcv 2895 . . . . . 6 โ„ฒ๐‘–(๐‘Ž๐‘€๐‘)
190188, 176, 189nfif 4550 . . . . 5 โ„ฒ๐‘–if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘))
191 eqeq1 2728 . . . . . . 7 (๐‘— = ๐‘Ž โ†’ (๐‘— = ๐ฟ โ†” ๐‘Ž = ๐ฟ))
192191adantr 480 . . . . . 6 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ (๐‘— = ๐ฟ โ†” ๐‘Ž = ๐ฟ))
193180adantl 481 . . . . . 6 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ ๐‘‹ = โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹)
194 oveq12 7410 . . . . . 6 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ (๐‘—๐‘€๐‘–) = (๐‘Ž๐‘€๐‘))
195192, 193, 194ifbieq12d 4548 . . . . 5 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)) = if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘)))
196185, 186, 187, 190, 195cbvmpo 7495 . . . 4 (๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘)))
197 iftrue 4526 . . . . . . . 8 (๐‘ โˆˆ ๐‘ โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹)
198197eqcomd 2730 . . . . . . 7 (๐‘ โˆˆ ๐‘ โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
199198adantl 481 . . . . . 6 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
200199ifeq1d 4539 . . . . 5 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
201200mpoeq3ia 7479 . . . 4 (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
202196, 201eqtri 2752 . . 3 (๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
203202fveq2i 6884 . 2 (๐ทโ€˜(๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
204174, 184, 2033eqtr4g 2789 1 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3053  Vcvv 3466  โฆ‹csb 3885   โˆ– cdif 3937   โˆช cun 3938   โІ wss 3940  โˆ…c0 4314  ifcif 4520  {csn 4620   โ†ฆ cmpt 5221   ร— cxp 5664  โŸถwf 6529  โ€˜cfv 6533  (class class class)co 7401   โˆˆ cmpo 7403   โ†‘m cmap 8815  Fincfn 8934  Basecbs 17140  +gcplusg 17193  .rcmulr 17194  0gc0g 17381   ฮฃg cgsu 17382  Mndcmnd 18654  CMndccmn 19685  1rcur 20071  Ringcrg 20123  CRingccrg 20124   Mat cmat 22217   maDet cmdat 22396   maAdju cmadu 22444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-addf 11184  ax-mulf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-xor 1505  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8698  df-map 8817  df-pm 8818  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-sup 9432  df-oi 9500  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-hash 14287  df-word 14461  df-lsw 14509  df-concat 14517  df-s1 14542  df-substr 14587  df-pfx 14617  df-splice 14696  df-reverse 14705  df-s2 14795  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18560  df-sgrp 18639  df-mnd 18655  df-mhm 18700  df-submnd 18701  df-efmnd 18781  df-grp 18853  df-minusg 18854  df-mulg 18983  df-subg 19035  df-ghm 19124  df-gim 19169  df-cntz 19218  df-oppg 19247  df-symg 19272  df-pmtr 19347  df-psgn 19396  df-cmn 19687  df-abl 19688  df-mgp 20025  df-rng 20043  df-ur 20072  df-ring 20125  df-cring 20126  df-oppr 20221  df-dvdsr 20244  df-unit 20245  df-invr 20275  df-dvr 20288  df-rhm 20359  df-subrng 20431  df-subrg 20456  df-drng 20574  df-sra 21006  df-rgmod 21007  df-cnfld 21224  df-zring 21297  df-zrh 21353  df-dsmm 21587  df-frlm 21602  df-mat 22218  df-mdet 22397  df-madu 22446
This theorem is referenced by:  madurid  22456  mdetlap1  33261
  Copyright terms: Public domain W3C validator