Theorem islshpsm

Description: Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014)

	Ref	Expression
Hypotheses	islshpsm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	islshpsm.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	islshpsm.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	islshpsm.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	islshpsm.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	islshpsm.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion	islshpsm	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islshpsm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		islshpsm.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		islshpsm.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4		islshpsm.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
5		islshpsm.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6		islshpsm.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7	1 2 3 5	islshp	⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
9	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ LMod )
10		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ∈ 𝑆 )
11	3 2	lspid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ 𝑈 ) = 𝑈 )
12	9 10 11	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) = 𝑈 )
13	12	uneq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) )
14	13	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
15	1 3	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
16	10 15	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ⊆ 𝑉 )
17		snssi	⊢ ( 𝑣 ∈ 𝑉 → { 𝑣 } ⊆ 𝑉 )
18	17	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → { 𝑣 } ⊆ 𝑉 )
19	1 2	lspun	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ { 𝑣 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
20	9 16 18 19	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
21	1 3 2	lspcl	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑣 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ 𝑆 )
22	9 18 21	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ 𝑆 )
23	3 2 4	lsmsp	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ ( 𝑁 ‘ { 𝑣 } ) ∈ 𝑆 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
24	9 10 22 23	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑣 } ) ) ) )
25	14 20 24	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) )
26	25	eqeq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ↔ ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
27	26	rexbidva	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ↔ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
28	27	pm5.32da	⊢ ( 𝜑 → ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
29	28	bicomd	⊢ ( 𝜑 → ( ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )
30		df-3an	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
31		df-3an	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) )
32	29 30 31	3bitr4g	⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )
33	8 32	bitrd	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑣 } ) ) = 𝑉 ) ) )