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

Hypotheses
Ref Expression
marep01ma.a 𝐴 = (𝑁 Mat 𝑅)
marep01ma.b 𝐵 = (Base‘𝐴)
marep01ma.r 𝑅 ∈ CRing
marep01ma.0 0 = (0g𝑅)
marep01ma.1 1 = (1r𝑅)
Assertion
Ref Expression
smadiadetlem3lem0 (((𝑀𝐵𝐾𝑁) ∧ 𝑄𝑊) → (((𝑌𝑍)‘𝑄)(.r𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑄𝑛))))) ∈ (Base‘𝑅))
Distinct variable groups:   𝑖,𝑗,𝑛,𝐵   𝑖,𝐾,𝑗,𝑛   𝑖,𝑀,𝑗,𝑛   𝑖,𝑁,𝑗,𝑛   𝑃,𝑖,𝑗,𝑛   𝑄,𝑖,𝑗,𝑛   𝑅,𝑖,𝑗,𝑛   1 ,𝑖,𝑗,𝑛   0 ,𝑖,𝑗,𝑛   𝑛,𝐺   𝑛,𝑊
Allowed substitution hints:   𝐴(𝑖,𝑗,𝑛)   𝑆(𝑖,𝑗,𝑛)   · (𝑖,𝑗,𝑛)   𝐺(𝑖,𝑗)   𝑊(𝑖,𝑗)   𝑌(𝑖,𝑗,𝑛)   𝑍(𝑖,𝑗,𝑛)

StepHypRef Expression
1 marep01ma.r . . 3 𝑅 ∈ CRing
21a1i 11 . 2 (((𝑀𝐵𝐾𝑁) ∧ 𝑄𝑊) → 𝑅 ∈ CRing)
3 difssd 3721 . . . . 5 (𝐾𝑁 → (𝑁 ∖ {𝐾}) ⊆ 𝑁)
43anim2i 592 . . . 4 ((𝑀𝐵𝐾𝑁) → (𝑀𝐵 ∧ (𝑁 ∖ {𝐾}) ⊆ 𝑁))
54adantr 481 . . 3 (((𝑀𝐵𝐾𝑁) ∧ 𝑄𝑊) → (𝑀𝐵 ∧ (𝑁 ∖ {𝐾}) ⊆ 𝑁))
6 marep01ma.a . . . 4 𝐴 = (𝑁 Mat 𝑅)
7 marep01ma.b . . . 4 𝐵 = (Base‘𝐴)
86, 7submabas 20316 . . 3 ((𝑀𝐵 ∧ (𝑁 ∖ {𝐾}) ⊆ 𝑁) → (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅)))
95, 8syl 17 . 2 (((𝑀𝐵𝐾𝑁) ∧ 𝑄𝑊) → (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗)) ∈ (Base‘((𝑁 ∖ {𝐾}) Mat 𝑅)))
10 simpr 477 . 2 (((𝑀𝐵𝐾𝑁) ∧ 𝑄𝑊) → 𝑄𝑊)