Metamath Proof Explorer

Theorem dsmmlss

Description: The finite hull of a product of modules is additionally closed under scalar multiplication and thus is a linear subspace of the product. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses dsmmlss.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
dsmmlss.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
dsmmlss.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
dsmmlss.k ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = 𝑆 )
dsmmlss.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
dsmmlss.u ⊢ 𝑈 = ( LSubSp ‘ 𝑃 )
dsmmlss.h ⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
Assertion dsmmlss ( 𝜑 → 𝐻 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 dsmmlss.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
2 dsmmlss.s ⊢ ( 𝜑 → 𝑆 ∈ Ring )
3 dsmmlss.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
4 dsmmlss.k ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = 𝑆 )
5 dsmmlss.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
6 dsmmlss.u ⊢ 𝑈 = ( LSubSp ‘ 𝑃 )
7 dsmmlss.h ⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
8 lmodgrp ⊢ ( 𝑎 ∈ LMod → 𝑎 ∈ Grp )
9 8 ssriv ⊢ LMod ⊆ Grp
10 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ LMod ∧ LMod ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp )
11 3 9 10 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
12 5 7 1 2 11 dsmmsubg ⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝑃 ) )
13 5 2 1 3 4 prdslmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → 𝑃 ∈ LMod )
15 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → 𝑏 ∈ 𝐻 )
17 eqid ⊢ ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 ⊕m 𝑅 )
18 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19 3 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
20 5 17 18 7 1 19 dsmmelbas ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐻 ↔ ( 𝑏 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑏 ∈ 𝐻 ↔ ( 𝑏 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) ) )
22 16 21 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑏 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) )
23 22 simpld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → 𝑏 ∈ ( Base ‘ 𝑃 ) )
24 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
25 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
26 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
27 18 24 25 26 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
28 14 15 23 27 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
29 22 simprd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → { 𝑥 ∈ 𝐼 ∣ ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin )
30 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ Ring )
32 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
33 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
34 fex ⊢ ( ( 𝑅 : 𝐼 ⟶ LMod ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
35 3 1 34 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
36 5 2 35 prdssca ⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑃 ) )
37 36 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
38 37 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑆 ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
39 38 biimpar ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
40 39 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
42 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑃 ) )
43 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
44 5 18 25 30 31 32 33 41 42 43 prdsvscafval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) )
45 44 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) )
46 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ LMod )
47 46 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ LMod )
48 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
49 36 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 = ( Scalar ‘ 𝑃 ) )
50 4 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Scalar ‘ 𝑃 ) )
51 50 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
52 51 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
53 48 52 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
54 eqid ⊢ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) )
55 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) )
56 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) )
57 eqid ⊢ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) )
58 54 55 56 57 lmodvs0 ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
59 47 53 58 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
60 oveq2 ⊢ ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
61 60 eqeq1d ⊢ ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ↔ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
62 59 61 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
63 62 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
64 45 63 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
65 64 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
66 65 necon3d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
67 66 ss2rabdv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ⊆ { 𝑥 ∈ 𝐼 ∣ ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
68 29 67 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin )
69 5 17 18 7 1 19 dsmmelbas ⊢ ( 𝜑 → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) ) )
71 28 68 70 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 )
72 71 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ 𝐻 ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 )
73 24 26 18 25 6 islss4 ⊢ ( 𝑃 ∈ LMod → ( 𝐻 ∈ 𝑈 ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ 𝐻 ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ) ) )
74 13 73 syl ⊢ ( 𝜑 → ( 𝐻 ∈ 𝑈 ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ 𝐻 ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ) ) )
75 12 72 74 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ 𝑈 )