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 3 1 fexd ⊢ ( 𝜑 → 𝑅 ∈ V )
35 5 2 34 prdssca ⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑃 ) )
36 35 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
37 36 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑆 ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
38 37 biimpar ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
39 38 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
41 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑃 ) )
42 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
43 5 18 25 30 31 32 33 40 41 42 prdsvscafval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) )
44 43 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) )
45 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ LMod )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ LMod )
47 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
48 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 = ( Scalar ‘ 𝑃 ) )
49 4 48 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Scalar ‘ 𝑃 ) )
50 49 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
51 50 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
52 47 51 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
53 eqid ⊢ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) )
54 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) )
55 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) )
56 eqid ⊢ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) )
57 53 54 55 56 lmodvs0 ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
58 46 52 57 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
59 oveq2 ⊢ ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
60 59 eqeq1d ⊢ ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ↔ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
61 58 60 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
62 61 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑏 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
63 44 62 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
64 63 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
65 64 necon3d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) → ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
66 65 ss2rabdv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ⊆ { 𝑥 ∈ 𝐼 ∣ ( 𝑏 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
67 29 66 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin )
68 5 17 18 7 1 19 dsmmelbas ⊢ ( 𝜑 → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) ) )
70 28 67 69 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 )
71 70 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ 𝐻 ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 )
72 24 26 18 25 6 islss4 ⊢ ( 𝑃 ∈ LMod → ( 𝐻 ∈ 𝑈 ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ 𝐻 ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ) ) )
73 13 72 syl ⊢ ( 𝜑 → ( 𝐻 ∈ 𝑈 ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ 𝐻 ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ) ) )
74 12 71 73 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ 𝑈 )