Metamath Proof Explorer

Theorem lmhmeql

Description: The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypothesis lmhmeql.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
Assertion lmhmeql ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lmhmeql.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
2 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
3 lmghm ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
4 ghmeql ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) )
5 2 3 4 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) )
6 fveq2 ⊢ ( 𝑧 = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) )
7 fveq2 ⊢ ( 𝑧 = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) )
8 6 7 eqeq12d ⊢ ( 𝑧 = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) )
9 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
10 9 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑆 ∈ LMod )
11 10 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑆 ∈ LMod )
12 simplr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
13 simprl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
14 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
15 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
16 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
17 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
18 14 15 16 17 lmodvscl ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
19 11 12 13 18 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
20 oveq2 ⊢ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
21 20 ad2antll ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
22 simplll ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
23 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
24 15 17 14 16 23 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
25 22 12 13 24 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
26 simpllr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) )
27 15 17 14 16 23 lmhmlin ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
28 26 12 13 27 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
29 21 25 28 3eqtr4d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) )
30 8 19 29 elrabd ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
31 30 expr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
32 31 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
33 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
34 14 33 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
35 34 ffnd ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
36 14 33 lmhmf ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
37 36 ffnd ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐺 Fn ( Base ‘ 𝑆 ) )
38 fndmin ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝐺 Fn ( Base ‘ 𝑆 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
39 35 37 38 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
40 39 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
41 eleq2 ⊢ ( dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
42 41 raleqbi1dv ⊢ ( dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } → ( ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
43 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
44 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑦 ) )
45 43 44 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
46 45 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
47 42 46 bitrdi ⊢ ( dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } → ( ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) ) )
48 40 47 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → ( ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) ) )
49 32 48 mpbird ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) )
50 49 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) )
51 15 17 14 16 1 islss4 ⊢ ( 𝑆 ∈ LMod → ( dom ( 𝐹 ∩ 𝐺 ) ∈ 𝑈 ↔ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ) ) )
52 10 51 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → ( dom ( 𝐹 ∩ 𝐺 ) ∈ 𝑈 ↔ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑦 ∈ dom ( 𝐹 ∩ 𝐺 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ) ) )
53 5 50 52 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ 𝑈 )