Metamath Proof Explorer

Theorem issubassa

Description: The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses issubassa.s ⊢ 𝑆 = ( 𝑊 ↾s 𝐴 )
issubassa.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
issubassa.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
issubassa.o ⊢ 1 = ( 1r ‘ 𝑊 )
Assertion issubassa ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ∈ AssAlg ↔ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 issubassa.s ⊢ 𝑆 = ( 𝑊 ↾s 𝐴 )
2 issubassa.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3 issubassa.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 issubassa.o ⊢ 1 = ( 1r ‘ 𝑊 )
5 simpl1 ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝑊 ∈ AssAlg )
6 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
7 5 6 syl ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝑊 ∈ Ring )
8 assaring ⊢ ( 𝑆 ∈ AssAlg → 𝑆 ∈ Ring )
9 8 adantl ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝑆 ∈ Ring )
10 1 9 eqeltrrid ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → ( 𝑊 ↾s 𝐴 ) ∈ Ring )
11 simpl3 ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝐴 ⊆ 𝑉 )
12 simpl2 ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 1 ∈ 𝐴 )
13 11 12 jca ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → ( 𝐴 ⊆ 𝑉 ∧ 1 ∈ 𝐴 ) )
14 3 4 issubrg ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ↔ ( ( 𝑊 ∈ Ring ∧ ( 𝑊 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝑉 ∧ 1 ∈ 𝐴 ) ) )
15 7 10 13 14 syl21anbrc ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝐴 ∈ ( SubRing ‘ 𝑊 ) )
16 assalmod ⊢ ( 𝑆 ∈ AssAlg → 𝑆 ∈ LMod )
17 16 adantl ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝑆 ∈ LMod )
18 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
19 1 3 2 islss3 ⊢ ( 𝑊 ∈ LMod → ( 𝐴 ∈ 𝐿 ↔ ( 𝐴 ⊆ 𝑉 ∧ 𝑆 ∈ LMod ) ) )
20 5 18 19 3syl ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → ( 𝐴 ∈ 𝐿 ↔ ( 𝐴 ⊆ 𝑉 ∧ 𝑆 ∈ LMod ) ) )
21 11 17 20 mpbir2and ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → 𝐴 ∈ 𝐿 )
22 15 21 jca ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ 𝑆 ∈ AssAlg ) → ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) )
23 1 2 issubassa3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ AssAlg )
24 23 3ad2antl1 ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ AssAlg )
25 22 24 impbida ⊢ ( ( 𝑊 ∈ AssAlg ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ∈ AssAlg ↔ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) )