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

Theorem mdetrlin 21903
Description: The determinant function is additive for each row: The matrices X, Y, Z are identical except for the I's row, and the I's row of the matrix X is the componentwise sum of the I's row of the matrices Y and Z. In this case the determinant of X is the sum of the determinants of Y and Z. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
Hypotheses
Ref Expression
mdetrlin.d 𝐷 = (𝑁 maDet 𝑅)
mdetrlin.a 𝐴 = (𝑁 Mat 𝑅)
mdetrlin.b 𝐵 = (Base‘𝐴)
mdetrlin.p + = (+g𝑅)
mdetrlin.r (𝜑𝑅 ∈ CRing)
mdetrlin.x (𝜑𝑋𝐵)
mdetrlin.y (𝜑𝑌𝐵)
mdetrlin.z (𝜑𝑍𝐵)
mdetrlin.i (𝜑𝐼𝑁)
mdetrlin.eq (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))
mdetrlin.ne1 (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
mdetrlin.ne2 (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
Assertion
Ref Expression
mdetrlin (𝜑 → (𝐷𝑋) = ((𝐷𝑌) + (𝐷𝑍)))

Proof of Theorem mdetrlin
Dummy variables 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6852 . . . . . 6 (Base‘(SymGrp‘𝑁)) ∈ V
2 ovex 7384 . . . . . . 7 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) ∈ V
3 eqid 2737 . . . . . . 7 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))))
42, 3fnmpti 6641 . . . . . 6 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) Fn (Base‘(SymGrp‘𝑁))
5 ovex 7384 . . . . . . 7 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) ∈ V
6 eqid 2737 . . . . . . 7 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))
75, 6fnmpti 6641 . . . . . 6 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) Fn (Base‘(SymGrp‘𝑁))
8 ofmpteq 7631 . . . . . 6 (((Base‘(SymGrp‘𝑁)) ∈ V ∧ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) Fn (Base‘(SymGrp‘𝑁)) ∧ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) Fn (Base‘(SymGrp‘𝑁))) → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))))
91, 4, 7, 8mp3an 1461 . . . . 5 ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
10 mdetrlin.r . . . . . . . . . 10 (𝜑𝑅 ∈ CRing)
11 crngring 19930 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
1210, 11syl 17 . . . . . . . . 9 (𝜑𝑅 ∈ Ring)
1312adantr 481 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
14 mdetrlin.y . . . . . . . . . . . . 13 (𝜑𝑌𝐵)
15 mdetrlin.a . . . . . . . . . . . . . 14 𝐴 = (𝑁 Mat 𝑅)
16 mdetrlin.b . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐴)
1715, 16matrcl 21711 . . . . . . . . . . . . 13 (𝑌𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
1814, 17syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
1918simpld 495 . . . . . . . . . . 11 (𝜑𝑁 ∈ Fin)
20 zrhpsgnmhm 20941 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
2112, 19, 20syl2anc 584 . . . . . . . . . 10 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
22 eqid 2737 . . . . . . . . . . 11 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
23 eqid 2737 . . . . . . . . . . . 12 (mulGrp‘𝑅) = (mulGrp‘𝑅)
24 eqid 2737 . . . . . . . . . . . 12 (Base‘𝑅) = (Base‘𝑅)
2523, 24mgpbas 19861 . . . . . . . . . . 11 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
2622, 25mhmf 18567 . . . . . . . . . 10 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
2721, 26syl 17 . . . . . . . . 9 (𝜑 → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶(Base‘𝑅))
2827ffvelcdmda 7031 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅))
2923crngmgp 19926 . . . . . . . . . . 11 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
3010, 29syl 17 . . . . . . . . . 10 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
3130adantr 481 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
3219adantr 481 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
3315, 24, 16matbas2i 21723 . . . . . . . . . . . . 13 (𝑌𝐵𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
34 elmapi 8745 . . . . . . . . . . . . 13 (𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
3514, 33, 343syl 18 . . . . . . . . . . . 12 (𝜑𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
3635ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
37 simpr 485 . . . . . . . . . . 11 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑟𝑁)
38 eqid 2737 . . . . . . . . . . . . . 14 (SymGrp‘𝑁) = (SymGrp‘𝑁)
3938, 22symgbasf 19116 . . . . . . . . . . . . 13 (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁𝑁)
4039adantl 482 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁𝑁)
4140ffvelcdmda 7031 . . . . . . . . . . 11 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑝𝑟) ∈ 𝑁)
4236, 37, 41fovcdmd 7520 . . . . . . . . . 10 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑟𝑌(𝑝𝑟)) ∈ (Base‘𝑅))
4342ralrimiva 3141 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟𝑁 (𝑟𝑌(𝑝𝑟)) ∈ (Base‘𝑅))
4425, 31, 32, 43gsummptcl 19703 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) ∈ (Base‘𝑅))
45 mdetrlin.z . . . . . . . . . . . . 13 (𝜑𝑍𝐵)
4615, 24, 16matbas2i 21723 . . . . . . . . . . . . 13 (𝑍𝐵𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
47 elmapi 8745 . . . . . . . . . . . . 13 (𝑍 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
4845, 46, 473syl 18 . . . . . . . . . . . 12 (𝜑𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
4948ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
5049, 37, 41fovcdmd 7520 . . . . . . . . . 10 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑟𝑍(𝑝𝑟)) ∈ (Base‘𝑅))
5150ralrimiva 3141 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟𝑁 (𝑟𝑍(𝑝𝑟)) ∈ (Base‘𝑅))
5225, 31, 32, 51gsummptcl 19703 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ (Base‘𝑅))
53 mdetrlin.p . . . . . . . . 9 + = (+g𝑅)
54 eqid 2737 . . . . . . . . 9 (.r𝑅) = (.r𝑅)
5524, 53, 54ringdi 19941 . . . . . . . 8 ((𝑅 ∈ Ring ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ (Base‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)(((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
5613, 28, 44, 52, 55syl13anc 1372 . . . . . . 7 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)(((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))
57 cmnmnd 19538 . . . . . . . . . . . . 13 ((mulGrp‘𝑅) ∈ CMnd → (mulGrp‘𝑅) ∈ Mnd)
5831, 57syl 17 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ Mnd)
59 mdetrlin.i . . . . . . . . . . . . 13 (𝜑𝐼𝑁)
6059adantr 481 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼𝑁)
6135adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑌:(𝑁 × 𝑁)⟶(Base‘𝑅))
6240, 60ffvelcdmd 7032 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑝𝐼) ∈ 𝑁)
6361, 60, 62fovcdmd 7520 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑌(𝑝𝐼)) ∈ (Base‘𝑅))
64 id 22 . . . . . . . . . . . . . 14 (𝑟 = 𝐼𝑟 = 𝐼)
65 fveq2 6839 . . . . . . . . . . . . . 14 (𝑟 = 𝐼 → (𝑝𝑟) = (𝑝𝐼))
6664, 65oveq12d 7369 . . . . . . . . . . . . 13 (𝑟 = 𝐼 → (𝑟𝑌(𝑝𝑟)) = (𝐼𝑌(𝑝𝐼)))
6725, 66gsumsn 19690 . . . . . . . . . . . 12 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼𝑁 ∧ (𝐼𝑌(𝑝𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) = (𝐼𝑌(𝑝𝐼)))
6858, 60, 63, 67syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) = (𝐼𝑌(𝑝𝐼)))
6968, 63eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) ∈ (Base‘𝑅))
7048adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑍:(𝑁 × 𝑁)⟶(Base‘𝑅))
7170, 60, 62fovcdmd 7520 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑍(𝑝𝐼)) ∈ (Base‘𝑅))
7264, 65oveq12d 7369 . . . . . . . . . . . . 13 (𝑟 = 𝐼 → (𝑟𝑍(𝑝𝑟)) = (𝐼𝑍(𝑝𝐼)))
7325, 72gsumsn 19690 . . . . . . . . . . . 12 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼𝑁 ∧ (𝐼𝑍(𝑝𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) = (𝐼𝑍(𝑝𝐼)))
7458, 60, 71, 73syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) = (𝐼𝑍(𝑝𝐼)))
7574, 71eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) ∈ (Base‘𝑅))
76 difssd 4090 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ⊆ 𝑁)
7732, 76ssfid 9169 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑁 ∖ {𝐼}) ∈ Fin)
78 eldifi 4084 . . . . . . . . . . . . 13 (𝑟 ∈ (𝑁 ∖ {𝐼}) → 𝑟𝑁)
79 mdetrlin.x . . . . . . . . . . . . . . . 16 (𝜑𝑋𝐵)
8015, 24, 16matbas2i 21723 . . . . . . . . . . . . . . . 16 (𝑋𝐵𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
81 elmapi 8745 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
8279, 80, 813syl 18 . . . . . . . . . . . . . . 15 (𝜑𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
8382ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
8483, 37, 41fovcdmd 7520 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟𝑁) → (𝑟𝑋(𝑝𝑟)) ∈ (Base‘𝑅))
8578, 84sylan2 593 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑋(𝑝𝑟)) ∈ (Base‘𝑅))
8685ralrimiva 3141 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑟 ∈ (𝑁 ∖ {𝐼})(𝑟𝑋(𝑝𝑟)) ∈ (Base‘𝑅))
8725, 31, 77, 86gsummptcl 19703 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))) ∈ (Base‘𝑅))
8824, 53, 54ringdir 19942 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))) ∈ (Base‘𝑅))) → ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))))))
8913, 69, 75, 87, 88syl13anc 1372 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))))))
9023, 54mgpplusg 19859 . . . . . . . . . . 11 (.r𝑅) = (+g‘(mulGrp‘𝑅))
91 disjdif 4429 . . . . . . . . . . . 12 ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅
9291a1i 11 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∩ (𝑁 ∖ {𝐼})) = ∅)
9359snssd 4767 . . . . . . . . . . . . . 14 (𝜑 → {𝐼} ⊆ 𝑁)
9493adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → {𝐼} ⊆ 𝑁)
95 undif 4439 . . . . . . . . . . . . 13 ({𝐼} ⊆ 𝑁 ↔ ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
9694, 95sylib 217 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} ∪ (𝑁 ∖ {𝐼})) = 𝑁)
9796eqcomd 2743 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 = ({𝐼} ∪ (𝑁 ∖ {𝐼})))
9825, 90, 31, 32, 84, 92, 97gsummptfidmsplit 19666 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
99 mdetrlin.eq . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))
10099adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))
101100oveqd 7368 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)))
102 xpss1 5650 . . . . . . . . . . . . . . . . . . 19 ({𝐼} ⊆ 𝑁 → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
10394, 102syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ⊆ (𝑁 × 𝑁))
10461, 103fssresd 6706 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅))
105104ffnd 6666 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
10670, 103fssresd 6706 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)):({𝐼} × 𝑁)⟶(Base‘𝑅))
107106ffnd 6666 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁))
108 snex 5386 . . . . . . . . . . . . . . . . 17 {𝐼} ∈ V
109 xpexg 7676 . . . . . . . . . . . . . . . . 17 (({𝐼} ∈ V ∧ 𝑁 ∈ Fin) → ({𝐼} × 𝑁) ∈ V)
110108, 32, 109sylancr 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ({𝐼} × 𝑁) ∈ V)
111 snidg 4618 . . . . . . . . . . . . . . . . . 18 (𝐼𝑁𝐼 ∈ {𝐼})
11260, 111syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝐼 ∈ {𝐼})
113112, 62opelxpd 5669 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ⟨𝐼, (𝑝𝐼)⟩ ∈ ({𝐼} × 𝑁))
114 fnfvof 7626 . . . . . . . . . . . . . . . 16 ((((𝑌 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁) ∧ (𝑍 ↾ ({𝐼} × 𝑁)) Fn ({𝐼} × 𝑁)) ∧ (({𝐼} × 𝑁) ∈ V ∧ ⟨𝐼, (𝑝𝐼)⟩ ∈ ({𝐼} × 𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝𝐼)⟩) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)))
115105, 107, 110, 113, 114syl22anc 837 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝𝐼)⟩) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)))
116 df-ov 7354 . . . . . . . . . . . . . . 15 (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)) = (((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))‘⟨𝐼, (𝑝𝐼)⟩)
117 df-ov 7354 . . . . . . . . . . . . . . . 16 (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = ((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)
118 df-ov 7354 . . . . . . . . . . . . . . . 16 (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩)
119117, 118oveq12i 7363 . . . . . . . . . . . . . . 15 ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))) = (((𝑌 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩) + ((𝑍 ↾ ({𝐼} × 𝑁))‘⟨𝐼, (𝑝𝐼)⟩))
120115, 116, 1193eqtr4g 2802 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))(𝑝𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))))
121101, 120eqtrd 2777 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))))
122 ovres 7514 . . . . . . . . . . . . . 14 ((𝐼 ∈ {𝐼} ∧ (𝑝𝐼) ∈ 𝑁) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑋(𝑝𝐼)))
123112, 62, 122syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑋 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑋(𝑝𝐼)))
124 ovres 7514 . . . . . . . . . . . . . . 15 ((𝐼 ∈ {𝐼} ∧ (𝑝𝐼) ∈ 𝑁) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑌(𝑝𝐼)))
125112, 62, 124syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑌(𝑝𝐼)))
126 ovres 7514 . . . . . . . . . . . . . . 15 ((𝐼 ∈ {𝐼} ∧ (𝑝𝐼) ∈ 𝑁) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑍(𝑝𝐼)))
127112, 62, 126syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) = (𝐼𝑍(𝑝𝐼)))
128125, 127oveq12d 7369 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((𝐼(𝑌 ↾ ({𝐼} × 𝑁))(𝑝𝐼)) + (𝐼(𝑍 ↾ ({𝐼} × 𝑁))(𝑝𝐼))) = ((𝐼𝑌(𝑝𝐼)) + (𝐼𝑍(𝑝𝐼))))
129121, 123, 1283eqtr3d 2785 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝𝐼)) = ((𝐼𝑌(𝑝𝐼)) + (𝐼𝑍(𝑝𝐼))))
13082adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑋:(𝑁 × 𝑁)⟶(Base‘𝑅))
131130, 60, 62fovcdmd 7520 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝐼𝑋(𝑝𝐼)) ∈ (Base‘𝑅))
13264, 65oveq12d 7369 . . . . . . . . . . . . . 14 (𝑟 = 𝐼 → (𝑟𝑋(𝑝𝑟)) = (𝐼𝑋(𝑝𝐼)))
13325, 132gsumsn 19690 . . . . . . . . . . . . 13 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼𝑁 ∧ (𝐼𝑋(𝑝𝐼)) ∈ (Base‘𝑅)) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) = (𝐼𝑋(𝑝𝐼)))
13458, 60, 131, 133syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) = (𝐼𝑋(𝑝𝐼)))
13568, 74oveq12d 7369 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))) = ((𝐼𝑌(𝑝𝐼)) + (𝐼𝑍(𝑝𝐼))))
136129, 134, 1353eqtr4d 2787 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))))
137136oveq1d 7366 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑋(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
13898, 137eqtrd 2777 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟)))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
13925, 90, 31, 32, 42, 92, 97gsummptfidmsplit 19666 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝𝑟))))))
140 mdetrlin.ne1 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
141140ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
142141oveqd 7368 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)))
143 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → 𝑟 ∈ (𝑁 ∖ {𝐼}))
14478, 41sylan2 593 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑝𝑟) ∈ 𝑁)
145 ovres 7514 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝𝑟) ∈ 𝑁) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑋(𝑝𝑟)))
146143, 144, 145syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑋(𝑝𝑟)))
147 ovres 7514 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝𝑟) ∈ 𝑁) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑌(𝑝𝑟)))
148143, 144, 147syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑌(𝑝𝑟)))
149142, 146, 1483eqtr3rd 2786 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑌(𝑝𝑟)) = (𝑟𝑋(𝑝𝑟)))
150149mpteq2dva 5203 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))
151150oveq2d 7367 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))))
152151oveq2d 7367 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑌(𝑝𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
153139, 152eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
15425, 90, 31, 32, 50, 92, 97gsummptfidmsplit 19666 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))))
155 mdetrlin.ne2 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
156155ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))
157156oveqd 7368 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)))
158 ovres 7514 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑁 ∖ {𝐼}) ∧ (𝑝𝑟) ∈ 𝑁) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑍(𝑝𝑟)))
159143, 144, 158syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟(𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))(𝑝𝑟)) = (𝑟𝑍(𝑝𝑟)))
160157, 146, 1593eqtr3rd 2786 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑟 ∈ (𝑁 ∖ {𝐼})) → (𝑟𝑍(𝑝𝑟)) = (𝑟𝑋(𝑝𝑟)))
161160mpteq2dva 5203 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))) = (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))
162161oveq2d 7367 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟)))) = ((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))))
163162oveq2d 7367 . . . . . . . . . . 11 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑍(𝑝𝑟))))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
164154, 163eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) = (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))))
165153, 164oveq12d 7369 . . . . . . . . 9 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = ((((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑌(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟))))) + (((mulGrp‘𝑅) Σg (𝑟 ∈ {𝐼} ↦ (𝑟𝑍(𝑝𝑟))))(.r𝑅)((mulGrp‘𝑅) Σg (𝑟 ∈ (𝑁 ∖ {𝐼}) ↦ (𝑟𝑋(𝑝𝑟)))))))
16689, 138, 1653eqtr4rd 2788 . . . . . . . 8 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) = ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))))
167166oveq2d 7367 . . . . . . 7 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)(((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) + ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))
16856, 167eqtr3d 2779 . . . . . 6 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))
169168mpteq2dva 5203 . . . . 5 (𝜑 → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) + ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))))))
1709, 169eqtrid 2789 . . . 4 (𝜑 → ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))) = (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟)))))))
171170oveq2d 7367 . . 3 (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))))
172 ringcmn 19956 . . . . 5 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
17310, 11, 1723syl 18 . . . 4 (𝜑𝑅 ∈ CMnd)
17438, 22symgbasfi 19119 . . . . 5 (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
17519, 174syl 17 . . . 4 (𝜑 → (Base‘(SymGrp‘𝑁)) ∈ Fin)
17624, 54ringcl 19935 . . . . 5 ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) ∈ (Base‘𝑅))
17713, 28, 44, 176syl3anc 1371 . . . 4 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))) ∈ (Base‘𝑅))
17824, 54ringcl 19935 . . . . 5 ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) ∈ (Base‘𝑅))
17913, 28, 52, 178syl3anc 1371 . . . 4 ((𝜑𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))) ∈ (Base‘𝑅))
18024, 53, 173, 175, 177, 179, 3, 6gsummptfidmadd2 19662 . . 3 (𝜑 → (𝑅 Σg ((𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟)))))) ∘f + (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
181171, 180eqtr3d 2779 . 2 (𝜑 → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
182 mdetrlin.d . . . 4 𝐷 = (𝑁 maDet 𝑅)
183 eqid 2737 . . . 4 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
184 eqid 2737 . . . 4 (pmSgn‘𝑁) = (pmSgn‘𝑁)
185182, 15, 16, 22, 183, 184, 54, 23mdetleib2 21889 . . 3 ((𝑅 ∈ CRing ∧ 𝑋𝐵) → (𝐷𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))))
18610, 79, 185syl2anc 584 . 2 (𝜑 → (𝐷𝑋) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑋(𝑝𝑟))))))))
187182, 15, 16, 22, 183, 184, 54, 23mdetleib2 21889 . . . 4 ((𝑅 ∈ CRing ∧ 𝑌𝐵) → (𝐷𝑌) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))))))
18810, 14, 187syl2anc 584 . . 3 (𝜑 → (𝐷𝑌) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))))))
189182, 15, 16, 22, 183, 184, 54, 23mdetleib2 21889 . . . 4 ((𝑅 ∈ CRing ∧ 𝑍𝐵) → (𝐷𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))))
19010, 45, 189syl2anc 584 . . 3 (𝜑 → (𝐷𝑍) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟))))))))
191188, 190oveq12d 7369 . 2 (𝜑 → ((𝐷𝑌) + (𝐷𝑍)) = ((𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑌(𝑝𝑟))))))) + (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑟𝑁 ↦ (𝑟𝑍(𝑝𝑟)))))))))
192181, 186, 1913eqtr4d 2787 1 (𝜑 → (𝐷𝑋) = ((𝐷𝑌) + (𝐷𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  Vcvv 3443  cdif 3905  cun 3906  cin 3907  wss 3908  c0 4280  {csn 4584  cop 4590  cmpt 5186   × cxp 5629  cres 5633  ccom 5635   Fn wfn 6488  wf 6489  cfv 6493  (class class class)co 7351  f cof 7607  m cmap 8723  Fincfn 8841  Basecbs 17043  +gcplusg 17093  .rcmulr 17094   Σg cgsu 17282  Mndcmnd 18516   MndHom cmhm 18559  SymGrpcsymg 19107  pmSgncpsgn 19230  CMndccmn 19521  mulGrpcmgp 19855  Ringcrg 19918  CRingccrg 19919  ℤRHomczrh 20853   Mat cmat 21706   maDet cmdat 21885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-addf 11088  ax-mulf 11089
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-xor 1510  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-om 7795  df-1st 7913  df-2nd 7914  df-supp 8085  df-tpos 8149  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-2o 8405  df-er 8606  df-map 8725  df-pm 8726  df-ixp 8794  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-fsupp 9264  df-sup 9336  df-oi 9404  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-4 12176  df-5 12177  df-6 12178  df-7 12179  df-8 12180  df-9 12181  df-n0 12372  df-xnn0 12444  df-z 12458  df-dec 12577  df-uz 12722  df-rp 12870  df-fz 13379  df-fzo 13522  df-seq 13861  df-exp 13922  df-hash 14185  df-word 14357  df-lsw 14405  df-concat 14413  df-s1 14438  df-substr 14487  df-pfx 14517  df-splice 14596  df-reverse 14605  df-s2 14695  df-struct 16979  df-sets 16996  df-slot 17014  df-ndx 17026  df-base 17044  df-ress 17073  df-plusg 17106  df-mulr 17107  df-starv 17108  df-sca 17109  df-vsca 17110  df-ip 17111  df-tset 17112  df-ple 17113  df-ds 17115  df-unif 17116  df-hom 17117  df-cco 17118  df-0g 17283  df-gsum 17284  df-prds 17289  df-pws 17291  df-mre 17426  df-mrc 17427  df-acs 17429  df-mgm 18457  df-sgrp 18506  df-mnd 18517  df-mhm 18561  df-submnd 18562  df-efmnd 18639  df-grp 18711  df-minusg 18712  df-mulg 18832  df-subg 18884  df-ghm 18965  df-gim 19008  df-cntz 19056  df-oppg 19083  df-symg 19108  df-pmtr 19183  df-psgn 19232  df-cmn 19523  df-abl 19524  df-mgp 19856  df-ur 19873  df-ring 19920  df-cring 19921  df-oppr 20002  df-dvdsr 20023  df-unit 20024  df-invr 20054  df-dvr 20065  df-rnghom 20099  df-drng 20140  df-subrg 20173  df-sra 20586  df-rgmod 20587  df-cnfld 20750  df-zring 20823  df-zrh 20857  df-dsmm 21091  df-frlm 21106  df-mat 21707  df-mdet 21886
This theorem is referenced by:  mdetrlin2  21908  mdetuni0  21922  mdetmul  21924
  Copyright terms: Public domain W3C validator