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

Theorem madugsum 22573
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 5245 . . . . 5 (๐‘ = โˆ… โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
21oveq2d 7442 . . . 4 (๐‘ = โˆ… โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
3 eleq2 2818 . . . . . . . 8 (๐‘ = โˆ… โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ โˆ…))
43ifbid 4555 . . . . . . 7 (๐‘ = โˆ… โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
54ifeq1d 4551 . . . . . 6 (๐‘ = โˆ… โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
65mpoeq3dv 7506 . . . . 5 (๐‘ = โˆ… โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
76fveq2d 6906 . . . 4 (๐‘ = โˆ… โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
82, 7eqeq12d 2744 . . 3 (๐‘ = โˆ… โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
9 mpteq1 5245 . . . . 5 (๐‘ = ๐‘‘ โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
109oveq2d 7442 . . . 4 (๐‘ = ๐‘‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
11 eleq2 2818 . . . . . . . 8 (๐‘ = ๐‘‘ โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ ๐‘‘))
1211ifbid 4555 . . . . . . 7 (๐‘ = ๐‘‘ โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
1312ifeq1d 4551 . . . . . 6 (๐‘ = ๐‘‘ โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
1413mpoeq3dv 7506 . . . . 5 (๐‘ = ๐‘‘ โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
1514fveq2d 6906 . . . 4 (๐‘ = ๐‘‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
1610, 15eqeq12d 2744 . . 3 (๐‘ = ๐‘‘ โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
17 mpteq1 5245 . . . . 5 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
1817oveq2d 7442 . . . 4 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
19 eleq2 2818 . . . . . . . 8 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ (๐‘‘ โˆช {๐‘’})))
2019ifbid 4555 . . . . . . 7 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
2120ifeq1d 4551 . . . . . 6 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
2221mpoeq3dv 7506 . . . . 5 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
2322fveq2d 6906 . . . 4 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
2418, 23eqeq12d 2744 . . 3 (๐‘ = (๐‘‘ โˆช {๐‘’}) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
25 mpteq1 5245 . . . . 5 (๐‘ = ๐‘ โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
2625oveq2d 7442 . . . 4 (๐‘ = ๐‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))))
27 eleq2 2818 . . . . . . . 8 (๐‘ = ๐‘ โ†’ (๐‘ โˆˆ ๐‘ โ†” ๐‘ โˆˆ ๐‘))
2827ifbid 4555 . . . . . . 7 (๐‘ = ๐‘ โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
2928ifeq1d 4551 . . . . . 6 (๐‘ = ๐‘ โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
3029mpoeq3dv 7506 . . . . 5 (๐‘ = ๐‘ โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
3130fveq2d 6906 . . . 4 (๐‘ = ๐‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
3226, 31eqeq12d 2744 . . 3 (๐‘ = ๐‘ โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†” (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
33 mpt0 6702 . . . . . 6 (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))) = โˆ…
3433oveq2i 7437 . . . . 5 (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg โˆ…)
35 eqid 2728 . . . . . 6 (0gโ€˜๐‘…) = (0gโ€˜๐‘…)
3635gsum0 18653 . . . . 5 (๐‘… ฮฃg โˆ…) = (0gโ€˜๐‘…)
3734, 36eqtri 2756 . . . 4 (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (0gโ€˜๐‘…)
38 noel 4334 . . . . . . . . 9 ยฌ ๐‘ โˆˆ โˆ…
39 iffalse 4541 . . . . . . . . 9 (ยฌ ๐‘ โˆˆ โˆ… โ†’ if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
4038, 39mp1i 13 . . . . . . . 8 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
4140ifeq1d 4551 . . . . . . 7 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘)))
4241mpoeq3ia 7505 . . . . . 6 (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘)))
4342fveq2i 6905 . . . . 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 22340 . . . . . . . 8 (๐‘€ โˆˆ ๐ต โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
5147, 50syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
5251simpld 493 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ Fin)
5348, 45, 49matbas2i 22352 . . . . . . . . 9 (๐‘€ โˆˆ ๐ต โ†’ ๐‘€ โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)))
54 elmapi 8876 . . . . . . . . 9 (๐‘€ โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ๐พ)
5547, 53, 543syl 18 . . . . . . . 8 (๐œ‘ โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ๐พ)
5655fovcdmda 7599 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘)) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
57563impb 1112 . . . . . 6 ((๐œ‘ โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
58 madugsum.l . . . . . 6 (๐œ‘ โ†’ ๐ฟ โˆˆ ๐‘)
5944, 45, 35, 46, 52, 57, 58mdetr0 22535 . . . . 5 (๐œ‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (0gโ€˜๐‘…), (๐‘Ž๐‘€๐‘)))) = (0gโ€˜๐‘…))
6043, 59eqtrid 2780 . . . 4 (๐œ‘ โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (0gโ€˜๐‘…))
6137, 60eqtr4id 2787 . . 3 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ โˆ… โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ โˆ…, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
62 eqid 2728 . . . . . . 7 (+gโ€˜๐‘…) = (+gโ€˜๐‘…)
6346adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ CRing)
64 crngring 20199 . . . . . . . . 9 (๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring)
6563, 64syl 17 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ Ring)
66 ringcmn 20232 . . . . . . . 8 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd)
6765, 66syl 17 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ CMnd)
6852adantr 479 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘ โˆˆ Fin)
69 simprl 769 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘‘ โІ ๐‘)
7068, 69ssfid 9300 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘‘ โˆˆ Fin)
7165adantr 479 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ ๐‘… โˆˆ Ring)
7269sselda 3982 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ ๐‘ โˆˆ ๐‘)
73 madugsum.x . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘– โˆˆ ๐‘) โ†’ ๐‘‹ โˆˆ ๐พ)
7473ralrimiva 3143 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
7574ad2antrr 724 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
76 rspcsbela 4439 . . . . . . . . 9 ((๐‘ โˆˆ ๐‘ โˆง โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
7772, 75, 76syl2anc 582 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
78 maduf.j . . . . . . . . . . . . . 14 ๐ฝ = (๐‘ maAdju ๐‘…)
7948, 78, 49maduf 22571 . . . . . . . . . . . . 13 (๐‘… โˆˆ CRing โ†’ ๐ฝ:๐ตโŸถ๐ต)
8046, 79syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ:๐ตโŸถ๐ต)
8180, 47ffvelcdmd 7100 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฝโ€˜๐‘€) โˆˆ ๐ต)
8248, 45, 49matbas2i 22352 . . . . . . . . . . 11 ((๐ฝโ€˜๐‘€) โˆˆ ๐ต โ†’ (๐ฝโ€˜๐‘€) โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)))
83 elmapi 8876 . . . . . . . . . . 11 ((๐ฝโ€˜๐‘€) โˆˆ (๐พ โ†‘m (๐‘ ร— ๐‘)) โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
8481, 82, 833syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
8584ad2antrr 724 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
8658ad2antrr 724 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ ๐ฟ โˆˆ ๐‘)
8785, 72, 86fovcdmd 7600 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ (๐‘(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ)
88 madugsum.t . . . . . . . . 9 ยท = (.rโ€˜๐‘…)
8945, 88ringcl 20204 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง (๐‘(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ) โ†’ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
9071, 77, 87, 89syl3anc 1368 . . . . . . 7 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ โˆˆ ๐‘‘) โ†’ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
91 vex 3477 . . . . . . . 8 ๐‘’ โˆˆ V
9291a1i 11 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘’ โˆˆ V)
93 eldifn 4128 . . . . . . . 8 (๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘) โ†’ ยฌ ๐‘’ โˆˆ ๐‘‘)
9493ad2antll 727 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ยฌ ๐‘’ โˆˆ ๐‘‘)
95 eldifi 4127 . . . . . . . . . 10 (๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘) โ†’ ๐‘’ โˆˆ ๐‘)
9695ad2antll 727 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘’ โˆˆ ๐‘)
9774adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
98 rspcsbela 4439 . . . . . . . . 9 ((๐‘’ โˆˆ ๐‘ โˆง โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ) โ†’ โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
9996, 97, 98syl2anc 582 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
10084adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ฝโ€˜๐‘€):(๐‘ ร— ๐‘)โŸถ๐พ)
10158adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐ฟ โˆˆ ๐‘)
102100, 96, 101fovcdmd 7600 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ)
10345, 88ringcl 20204 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
10465, 99, 102, 103syl3anc 1368 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)) โˆˆ ๐พ)
105 csbeq1 3897 . . . . . . . 8 (๐‘ = ๐‘’ โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
106 oveq1 7433 . . . . . . . 8 (๐‘ = ๐‘’ โ†’ (๐‘(๐ฝโ€˜๐‘€)๐ฟ) = (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))
107105, 106oveq12d 7444 . . . . . . 7 (๐‘ = ๐‘’ โ†’ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)))
10845, 62, 67, 70, 90, 92, 94, 104, 107gsumunsn 19929 . . . . . 6 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
109108adantr 479 . . . . 5 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
110 oveq1 7433 . . . . . 6 ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
111110adantl 480 . . . . 5 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
112 elun 4149 . . . . . . . . . . . . . 14 (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ โˆˆ {๐‘’}))
113 velsn 4648 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ {๐‘’} โ†” ๐‘ = ๐‘’)
114113orbi2i 910 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ โˆˆ {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’))
115112, 114bitri 274 . . . . . . . . . . . . 13 (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’))
116 ifbi 4554 . . . . . . . . . . . . 13 ((๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†” (๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’)) โ†’ if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
117115, 116ax-mp 5 . . . . . . . . . . . 12 if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))
118 ringmnd 20197 . . . . . . . . . . . . . . 15 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd)
11965, 118syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘… โˆˆ Mnd)
1201193ad2ant1 1130 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘… โˆˆ Mnd)
121 simp3 1135 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ ๐‘)
122973ad2ant1 1130 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ โˆ€๐‘– โˆˆ ๐‘ ๐‘‹ โˆˆ ๐พ)
123121, 122, 76syl2anc 582 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ)
124 elequ1 2105 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘’ โ†’ (๐‘ โˆˆ ๐‘‘ โ†” ๐‘’ โˆˆ ๐‘‘))
125124biimpac 477 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’) โ†’ ๐‘’ โˆˆ ๐‘‘)
12694, 125nsyl 140 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ยฌ (๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’))
1271263ad2ant1 1130 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ยฌ (๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’))
12845, 35, 62mndifsplit 22566 . . . . . . . . . . . . 13 ((๐‘… โˆˆ Mnd โˆง โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง ยฌ (๐‘ โˆˆ ๐‘‘ โˆง ๐‘ = ๐‘’)) โ†’ if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))))
129120, 123, 127, 128syl3anc 1368 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if((๐‘ โˆˆ ๐‘‘ โˆจ ๐‘ = ๐‘’), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))))
130117, 129eqtrid 2780 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))))
131105adantl 480 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘ = ๐‘’) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
132131ifeq1da 4563 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = if(๐‘ = ๐‘’, โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
133 ovif2 7526 . . . . . . . . . . . . . . 15 (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) = if(๐‘ = ๐‘’, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)), (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…)))
134 eqid 2728 . . . . . . . . . . . . . . . . . 18 (1rโ€˜๐‘…) = (1rโ€˜๐‘…)
13545, 88, 134ringridm 20220 . . . . . . . . . . . . . . . . 17 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)) = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
13665, 99, 135syl2anc 582 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)) = โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹)
13745, 88, 35ringrz 20244 . . . . . . . . . . . . . . . . 17 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
13865, 99, 137syl2anc 582 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…)) = (0gโ€˜๐‘…))
139136, 138ifeq12d 4553 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (1rโ€˜๐‘…)), (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (0gโ€˜๐‘…))) = if(๐‘ = ๐‘’, โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
140133, 139eqtrid 2780 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) = if(๐‘ = ๐‘’, โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
141132, 140eqtr4d 2771 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))))
142141oveq2d 7442 . . . . . . . . . . . 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 2768 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))))
145144ifeq1d 4551 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘)))
146145mpoeq3dva 7504 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘))))
147146fveq2d 6906 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)))), (๐‘Ž๐‘€๐‘)))))
14845, 35ring0cl 20217 . . . . . . . . . . 11 (๐‘… โˆˆ Ring โ†’ (0gโ€˜๐‘…) โˆˆ ๐พ)
14965, 148syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (0gโ€˜๐‘…) โˆˆ ๐พ)
1501493ad2ant1 1130 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (0gโ€˜๐‘…) โˆˆ ๐พ)
151123, 150ifcld 4578 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) โˆˆ ๐พ)
15245, 134ringidcl 20216 . . . . . . . . . . . 12 (๐‘… โˆˆ Ring โ†’ (1rโ€˜๐‘…) โˆˆ ๐พ)
15365, 152syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (1rโ€˜๐‘…) โˆˆ ๐พ)
154153, 149ifcld 4578 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)) โˆˆ ๐พ)
15545, 88ringcl 20204 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ โˆˆ ๐พ โˆง if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)) โˆˆ ๐พ) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) โˆˆ ๐พ)
15665, 99, 154, 155syl3anc 1368 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) โˆˆ ๐พ)
1571563ad2ant1 1130 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))) โˆˆ ๐พ)
15855adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ๐พ)
159158fovcdmda 7599 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘)) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
1601593impb 1112 . . . . . . . 8 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง ๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘Ž๐‘€๐‘) โˆˆ ๐พ)
16144, 45, 62, 63, 68, 151, 157, 160, 101mdetrlin2 22537 . . . . . . 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 22534 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘)))) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
16447adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ๐‘€ โˆˆ ๐ต)
16548, 44, 78, 49, 134, 35maducoeval 22569 . . . . . . . . . . 11 ((๐‘€ โˆˆ ๐ต โˆง ๐‘’ โˆˆ ๐‘ โˆง ๐ฟ โˆˆ ๐‘) โ†’ (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
166164, 96, 101, 165syl3anc 1368 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐‘’(๐ฝโ€˜๐‘€)๐ฟ) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
167166oveq2d 7442 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
168163, 167eqtr4d 2771 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘)))) = (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ)))
169168oveq2d 7442 . . . . . . 7 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, (โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท if(๐‘ = ๐‘’, (1rโ€˜๐‘…), (0gโ€˜๐‘…))), (๐‘Ž๐‘€๐‘))))) = ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))))
170147, 161, 1693eqtrrd 2773 . . . . . 6 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
171170adantr 479 . . . . 5 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ ((๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))(+gโ€˜๐‘…)(โฆ‹๐‘’ / ๐‘–โฆŒ๐‘‹ ยท (๐‘’(๐ฝโ€˜๐‘€)๐ฟ))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
172109, 111, 1713eqtrd 2772 . . . 4 (((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โˆง (๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
173172ex 411 . . 3 ((๐œ‘ โˆง (๐‘‘ โІ ๐‘ โˆง ๐‘’ โˆˆ (๐‘ โˆ– ๐‘‘))) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ ๐‘‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))) โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}) โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ (๐‘‘ โˆช {๐‘’}), โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))))
1748, 16, 24, 32, 61, 173, 52findcard2d 9199 . 2 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))))
175 nfcv 2899 . . . 4 โ„ฒ๐‘(๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ))
176 nfcsb1v 3919 . . . . 5 โ„ฒ๐‘–โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹
177 nfcv 2899 . . . . 5 โ„ฒ๐‘– ยท
178 nfcv 2899 . . . . 5 โ„ฒ๐‘–(๐‘(๐ฝโ€˜๐‘€)๐ฟ)
179176, 177, 178nfov 7456 . . . 4 โ„ฒ๐‘–(โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))
180 csbeq1a 3908 . . . . 5 (๐‘– = ๐‘ โ†’ ๐‘‹ = โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹)
181 oveq1 7433 . . . . 5 (๐‘– = ๐‘ โ†’ (๐‘–(๐ฝโ€˜๐‘€)๐ฟ) = (๐‘(๐ฝโ€˜๐‘€)๐ฟ))
182180, 181oveq12d 7444 . . . 4 (๐‘– = ๐‘ โ†’ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)) = (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))
183175, 179, 182cbvmpt 5263 . . 3 (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ))) = (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ)))
184183oveq2i 7437 . 2 (๐‘… ฮฃg (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ ยท (๐‘(๐ฝโ€˜๐‘€)๐ฟ))))
185 nfcv 2899 . . . . 5 โ„ฒ๐‘Žif(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))
186 nfcv 2899 . . . . 5 โ„ฒ๐‘if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))
187 nfcv 2899 . . . . 5 โ„ฒ๐‘—if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘))
188 nfv 1909 . . . . . 6 โ„ฒ๐‘– ๐‘Ž = ๐ฟ
189 nfcv 2899 . . . . . 6 โ„ฒ๐‘–(๐‘Ž๐‘€๐‘)
190188, 176, 189nfif 4562 . . . . 5 โ„ฒ๐‘–if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘))
191 eqeq1 2732 . . . . . . 7 (๐‘— = ๐‘Ž โ†’ (๐‘— = ๐ฟ โ†” ๐‘Ž = ๐ฟ))
192191adantr 479 . . . . . 6 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ (๐‘— = ๐ฟ โ†” ๐‘Ž = ๐ฟ))
193180adantl 480 . . . . . 6 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ ๐‘‹ = โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹)
194 oveq12 7435 . . . . . 6 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ (๐‘—๐‘€๐‘–) = (๐‘Ž๐‘€๐‘))
195192, 193, 194ifbieq12d 4560 . . . . 5 ((๐‘— = ๐‘Ž โˆง ๐‘– = ๐‘) โ†’ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)) = if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘)))
196185, 186, 187, 190, 195cbvmpo 7521 . . . 4 (๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘)))
197 iftrue 4538 . . . . . . . 8 (๐‘ โˆˆ ๐‘ โ†’ if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)) = โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹)
198197eqcomd 2734 . . . . . . 7 (๐‘ โˆˆ ๐‘ โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
199198adantl 480 . . . . . 6 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹ = if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)))
200199ifeq1d 4551 . . . . 5 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘)) = if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
201200mpoeq3ia 7505 . . . 4 (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (๐‘Ž๐‘€๐‘))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
202196, 201eqtri 2756 . . 3 (๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–))) = (๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘)))
203202fveq2i 6905 . 2 (๐ทโ€˜(๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)))) = (๐ทโ€˜(๐‘Ž โˆˆ ๐‘, ๐‘ โˆˆ ๐‘ โ†ฆ if(๐‘Ž = ๐ฟ, if(๐‘ โˆˆ ๐‘, โฆ‹๐‘ / ๐‘–โฆŒ๐‘‹, (0gโ€˜๐‘…)), (๐‘Ž๐‘€๐‘))))
204174, 184, 2033eqtr4g 2793 1 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘– โˆˆ ๐‘ โ†ฆ (๐‘‹ ยท (๐‘–(๐ฝโ€˜๐‘€)๐ฟ)))) = (๐ทโ€˜(๐‘— โˆˆ ๐‘, ๐‘– โˆˆ ๐‘ โ†ฆ if(๐‘— = ๐ฟ, ๐‘‹, (๐‘—๐‘€๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 845   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3058  Vcvv 3473  โฆ‹csb 3894   โˆ– cdif 3946   โˆช cun 3947   โІ wss 3949  โˆ…c0 4326  ifcif 4532  {csn 4632   โ†ฆ cmpt 5235   ร— cxp 5680  โŸถwf 6549  โ€˜cfv 6553  (class class class)co 7426   โˆˆ cmpo 7428   โ†‘m cmap 8853  Fincfn 8972  Basecbs 17189  +gcplusg 17242  .rcmulr 17243  0gc0g 17430   ฮฃg cgsu 17431  Mndcmnd 18703  CMndccmn 19749  1rcur 20135  Ringcrg 20187  CRingccrg 20188   Mat cmat 22335   maDet cmdat 22514   maAdju cmadu 22562
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 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-addf 11227  ax-mulf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  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 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-ot 4641  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7879  df-1st 8001  df-2nd 8002  df-supp 8174  df-tpos 8240  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-er 8733  df-map 8855  df-pm 8856  df-ixp 8925  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-fsupp 9396  df-sup 9475  df-oi 9543  df-card 9972  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-xnn0 12585  df-z 12599  df-dec 12718  df-uz 12863  df-rp 13017  df-fz 13527  df-fzo 13670  df-seq 14009  df-exp 14069  df-hash 14332  df-word 14507  df-lsw 14555  df-concat 14563  df-s1 14588  df-substr 14633  df-pfx 14663  df-splice 14742  df-reverse 14751  df-s2 14841  df-struct 17125  df-sets 17142  df-slot 17160  df-ndx 17172  df-base 17190  df-ress 17219  df-plusg 17255  df-mulr 17256  df-starv 17257  df-sca 17258  df-vsca 17259  df-ip 17260  df-tset 17261  df-ple 17262  df-ds 17264  df-unif 17265  df-hom 17266  df-cco 17267  df-0g 17432  df-gsum 17433  df-prds 17438  df-pws 17440  df-mre 17575  df-mrc 17576  df-acs 17578  df-mgm 18609  df-sgrp 18688  df-mnd 18704  df-mhm 18749  df-submnd 18750  df-efmnd 18835  df-grp 18907  df-minusg 18908  df-mulg 19038  df-subg 19092  df-ghm 19182  df-gim 19227  df-cntz 19282  df-oppg 19311  df-symg 19336  df-pmtr 19411  df-psgn 19460  df-cmn 19751  df-abl 19752  df-mgp 20089  df-rng 20107  df-ur 20136  df-ring 20189  df-cring 20190  df-oppr 20287  df-dvdsr 20310  df-unit 20311  df-invr 20341  df-dvr 20354  df-rhm 20425  df-subrng 20497  df-subrg 20522  df-drng 20640  df-sra 21072  df-rgmod 21073  df-cnfld 21294  df-zring 21387  df-zrh 21443  df-dsmm 21680  df-frlm 21695  df-mat 22336  df-mdet 22515  df-madu 22564
This theorem is referenced by:  madurid  22574  mdetlap1  33468
  Copyright terms: Public domain W3C validator