Description: Lemma for isdrng3 : The base set of a multipication group restricted to a subset of the original base set. (Contributed by AV, 22-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | isdrng3.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| Assertion | isdrng3lem0 | ⊢ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ 𝑋 ) ) ) = ( 𝐵 ∖ 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isdrng3.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| 2 | difss | ⊢ ( 𝐵 ∖ 𝑋 ) ⊆ 𝐵 | |
| 3 | eqid | ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ 𝑋 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ 𝑋 ) ) | |
| 4 | eqid | ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) | |
| 5 | 4 1 | mgpbas | ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) |
| 6 | 3 5 | ressbas2 | ⊢ ( ( 𝐵 ∖ 𝑋 ) ⊆ 𝐵 → ( 𝐵 ∖ 𝑋 ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ 𝑋 ) ) ) ) |
| 7 | 6 | eqcomd | ⊢ ( ( 𝐵 ∖ 𝑋 ) ⊆ 𝐵 → ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ 𝑋 ) ) ) = ( 𝐵 ∖ 𝑋 ) ) |
| 8 | 2 7 | ax-mp | ⊢ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ 𝑋 ) ) ) = ( 𝐵 ∖ 𝑋 ) |