Theorem sdrgunit

Description: A unit of a sub-division-ring is a nonzero element of the subring. (Contributed by SN, 19-Feb-2025)

	Ref	Expression
Hypotheses	sdrgunit.s	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
	sdrgunit.0	⊢ 0 = ( 0g ‘ 𝑅 )
	sdrgunit.u	⊢ 𝑈 = ( Unit ‘ 𝑆 )
Assertion	sdrgunit	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sdrgunit.s	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		sdrgunit.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		sdrgunit.u	⊢ 𝑈 = ( Unit ‘ 𝑆 )
4	1	sdrgdrng	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 𝑆 ∈ DivRing )
5		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
7	5 3 6	drngunit	⊢ ( 𝑆 ∈ DivRing → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ) )
8	4 7	syl	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ) )
9	1	sdrgbas	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
10	9	eleq2d	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑋 ∈ 𝐴 ↔ 𝑋 ∈ ( Base ‘ 𝑆 ) ) )
11		sdrgsubrg	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
12	1 2	subrg0	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )
13	11 12	syl	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )
14	13	neeq2d	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑋 ≠ 0 ↔ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) )
15	10 14	anbi12d	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑆 ) ) ) )
16	8 15	bitr4d	⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) ) )