Step |
Hyp |
Ref |
Expression |
1 |
|
prdsmndd.y |
⊢ 𝑌 = ( 𝑆 Xs 𝑅 ) |
2 |
|
prdsmndd.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
3 |
|
prdsmndd.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) |
4 |
|
prdsmndd.r |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 ) |
6 |
|
eqid |
⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) |
7 |
3
|
elexd |
⊢ ( 𝜑 → 𝑆 ∈ V ) |
8 |
2
|
elexd |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
9 |
|
eqid |
⊢ ( 0g ∘ 𝑅 ) = ( 0g ∘ 𝑅 ) |
10 |
1 5 6 7 8 4 9
|
prdsidlem |
⊢ ( 𝜑 → ( ( 0g ∘ 𝑅 ) ∈ ( Base ‘ 𝑌 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑏 ) ) ) |
11 |
|
eqid |
⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 ) |
12 |
1 2 3 4
|
prdsmndd |
⊢ ( 𝜑 → 𝑌 ∈ Mnd ) |
13 |
5 6
|
mndid |
⊢ ( 𝑌 ∈ Mnd → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) 𝑎 ) = 𝑏 ) ) |
14 |
12 13
|
syl |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) 𝑎 ) = 𝑏 ) ) |
15 |
5 11 6 14
|
ismgmid |
⊢ ( 𝜑 → ( ( ( 0g ∘ 𝑅 ) ∈ ( Base ‘ 𝑌 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑏 ) ) ↔ ( 0g ‘ 𝑌 ) = ( 0g ∘ 𝑅 ) ) ) |
16 |
10 15
|
mpbid |
⊢ ( 𝜑 → ( 0g ‘ 𝑌 ) = ( 0g ∘ 𝑅 ) ) |
17 |
16
|
eqcomd |
⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑌 ) ) |