Metamath Proof Explorer

Theorem islshpat

Description: Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm . (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses islshpat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islshpat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
islshpat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
islshpat.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
islshpat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
islshpat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion islshpat ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 islshpat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 islshpat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 islshpat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 islshpat.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5 islshpat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
6 islshpat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
8 1 7 2 3 4 6 islshpsm ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
9 df-3an ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
10 r19.42v ⊢ ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
11 9 10 bitr4i ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
12 df-rex ⊢ ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
13 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → 𝑣 = ( 0g ‘ 𝑊 ) )
14 13 sneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → { 𝑣 } = { ( 0g ‘ 𝑊 ) } )
15 14 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = ( ( LSpan ‘ 𝑊 ) ‘ { ( 0g ‘ 𝑊 ) } ) )
16 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → 𝑊 ∈ LMod )
17 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
18 17 7 lspsn0 ⊢ ( 𝑊 ∈ LMod → ( ( LSpan ‘ 𝑊 ) ‘ { ( 0g ‘ 𝑊 ) } ) = { ( 0g ‘ 𝑊 ) } )
19 16 18 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 0g ‘ 𝑊 ) } ) = { ( 0g ‘ 𝑊 ) } )
20 15 19 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { ( 0g ‘ 𝑊 ) } )
21 20 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = ( 𝑈 ⊕ { ( 0g ‘ 𝑊 ) } ) )
22 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → 𝑈 ∈ 𝑆 )
23 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
24 16 22 23 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
25 17 3 lsm01 ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → ( 𝑈 ⊕ { ( 0g ‘ 𝑊 ) } ) = 𝑈 )
26 24 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( 𝑈 ⊕ { ( 0g ‘ 𝑊 ) } ) = 𝑈 )
27 21 26 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑈 )
28 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → 𝑈 ≠ 𝑉 )
29 27 28 eqnetrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 = ( 0g ‘ 𝑊 ) ) → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ≠ 𝑉 )
30 29 ex ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) → ( 𝑣 = ( 0g ‘ 𝑊 ) → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ≠ 𝑉 ) )
31 30 necon2d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) → ( ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 → 𝑣 ≠ ( 0g ‘ 𝑊 ) ) )
32 31 pm4.71rd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) → ( ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ↔ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
33 32 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
34 33 pm5.32da ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) ) )
35 eldifsn ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ↔ ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) )
36 35 anbi1i ⊢ ( ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
37 anass ⊢ ( ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
38 an12 ⊢ ( ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
39 38 anbi2i ⊢ ( ( 𝑣 ∈ 𝑉 ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
40 37 39 bitri ⊢ ( ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
41 36 40 bitr2i ⊢ ( ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑣 ≠ ( 0g ‘ 𝑊 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) ↔ ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
42 34 41 bitrdi ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
43 42 exbidv ⊢ ( 𝜑 → ( ∃ 𝑣 ( 𝑣 ∈ 𝑉 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
44 12 43 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
45 fvex ⊢ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∈ V
46 45 rexcom4b ⊢ ( ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ∧ 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
47 df-rex ⊢ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
48 46 47 bitr2i ⊢ ( ∃ 𝑣 ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ∧ 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
49 ancom ⊢ ( ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ∧ 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ↔ ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
50 49 rexbii ⊢ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ∧ 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
51 50 exbii ⊢ ( ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ∧ 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ↔ ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
52 48 51 bitri ⊢ ( ∃ 𝑣 ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ↔ ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
53 44 52 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) ) )
54 r19.41v ⊢ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) )
55 oveq2 ⊢ ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑈 ⊕ 𝑞 ) = ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
56 55 eqeq1d ⊢ ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( 𝑈 ⊕ 𝑞 ) = 𝑉 ↔ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
57 56 anbi2d ⊢ ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
58 57 pm5.32i ⊢ ( ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
59 58 rexbii ⊢ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
60 54 59 bitr3i ⊢ ( ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
61 60 exbii ⊢ ( ∃ 𝑞 ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ∃ 𝑞 ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
62 53 61 bitr4di ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑞 ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ) )
63 1 7 17 5 islsat ⊢ ( 𝑊 ∈ LMod → ( 𝑞 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
64 6 63 syl ⊢ ( 𝜑 → ( 𝑞 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
65 64 anbi1d ⊢ ( 𝜑 → ( ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ) )
66 65 exbidv ⊢ ( 𝜑 → ( ∃ 𝑞 ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ∃ 𝑞 ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ) )
67 62 66 bitr4d ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑞 ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ) )
68 11 67 syl5bb ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ∃ 𝑞 ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ) )
69 df-3an ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) )
70 r19.42v ⊢ ( ∃ 𝑞 ∈ 𝐴 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) )
71 df-rex ⊢ ( ∃ 𝑞 ∈ 𝐴 ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ↔ ∃ 𝑞 ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) )
72 70 71 bitr3i ⊢ ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ↔ ∃ 𝑞 ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) )
73 69 72 bitr2i ⊢ ( ∃ 𝑞 ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) )
74 68 73 bitrdi ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) )
75 8 74 bitrd ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑈 ⊕ 𝑞 ) = 𝑉 ) ) )