Metamath Proof Explorer

Theorem issubassa2

Description: A subring of a unital algebra is a subspace and thus a subalgebra iff it contains all scalar multiples of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses issubassa2.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
issubassa2.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion issubassa2 ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑆 ∈ 𝐿 ↔ ran 𝐴 ⊆ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issubassa2.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 issubassa2.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
4 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
5 1 3 4 rnascl ⊢ ( 𝑊 ∈ AssAlg → ran 𝐴 = ( ( LSpan ‘ 𝑊 ) ‘ { ( 1r ‘ 𝑊 ) } ) )
6 5 ad2antrr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ 𝑆 ∈ 𝐿 ) → ran 𝐴 = ( ( LSpan ‘ 𝑊 ) ‘ { ( 1r ‘ 𝑊 ) } ) )
7 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
8 7 ad2antrr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ 𝑆 ∈ 𝐿 ) → 𝑊 ∈ LMod )
9 simpr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ 𝑆 ∈ 𝐿 ) → 𝑆 ∈ 𝐿 )
10 3 subrg1cl ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 1r ‘ 𝑊 ) ∈ 𝑆 )
11 10 ad2antlr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ 𝑆 ∈ 𝐿 ) → ( 1r ‘ 𝑊 ) ∈ 𝑆 )
12 2 4 8 9 11 lspsnel5a ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ 𝑆 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 1r ‘ 𝑊 ) } ) ⊆ 𝑆 )
13 6 12 eqsstrd ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ 𝑆 ∈ 𝐿 ) → ran 𝐴 ⊆ 𝑆 )
14 subrgsubg ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ∈ ( SubGrp ‘ 𝑊 ) )
15 14 ad2antlr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝑊 ) )
16 simplll ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑊 ∈ AssAlg )
17 simprl ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
19 18 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
20 19 ad2antlr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
21 20 sselda ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
22 21 adantrl ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
23 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
24 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
25 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
26 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
27 1 23 24 18 25 26 asclmul1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
28 16 17 22 27 syl3anc ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
29 simpllr ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑊 ) )
30 simplr ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ran 𝐴 ⊆ 𝑆 )
31 1 23 24 asclfn ⊢ 𝐴 Fn ( Base ‘ ( Scalar ‘ 𝑊 ) )
32 31 a1i ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) → 𝐴 Fn ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
33 fnfvelrn ⊢ ( ( 𝐴 Fn ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ran 𝐴 )
34 32 33 sylan ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ran 𝐴 )
35 30 34 sseldd ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑆 )
36 35 adantrr ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑆 )
37 simprr ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
38 25 subrgmcl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 )
39 29 36 37 38 syl3anc ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 )
40 28 39 eqeltrrd ⊢ ( ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 )
41 40 ralrimivva ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 )
42 23 24 18 26 2 islss4 ⊢ ( 𝑊 ∈ LMod → ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 ) ) )
43 7 42 syl ⊢ ( 𝑊 ∈ AssAlg → ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 ) ) )
44 43 ad2antrr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) → ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑆 ) ) )
45 15 41 44 mpbir2and ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ran 𝐴 ⊆ 𝑆 ) → 𝑆 ∈ 𝐿 )
46 13 45 impbida ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑆 ∈ 𝐿 ↔ ran 𝐴 ⊆ 𝑆 ) )