Metamath Proof Explorer

Theorem dihjat1lem

Description: Subspace sum of a closed subspace and an atom. ( pmapjat1 analog.) TODO: merge into dihjat1 ? (Contributed by NM, 18-Aug-2014)

Ref Expression
Hypotheses dihjat1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihjat1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjat1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dihjat1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihjat1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihjat1.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihjat1.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
dihjat1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihjat1.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dihjat1.o ⊢ 0 = ( 0g ‘ 𝑈 )
dihjat1lem.q ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion dihjat1lem ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )

Proof

Step Hyp Ref Expression
1 dihjat1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihjat1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihjat1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dihjat1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
5 dihjat1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 dihjat1.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 dihjat1.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
8 dihjat1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dihjat1.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
10 dihjat1.o ⊢ 0 = ( 0g ‘ 𝑈 )
11 dihjat1lem.q ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = { 0 } ) → 𝑋 = { 0 } )
13 12 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 = { 0 } ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( { 0 } ∨ ( 𝑁 ‘ { 𝑇 } ) ) )
14 12 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 = { 0 } ) → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) = ( { 0 } ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
15 eldifi ⊢ ( 𝑇 ∈ ( 𝑉 ∖ { 0 } ) → 𝑇 ∈ 𝑉 )
16 11 15 syl ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
17 1 2 3 5 6 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑇 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑇 } ) ∈ ran 𝐼 )
18 8 16 17 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ∈ ran 𝐼 )
19 1 2 10 6 7 8 18 djh02 ⊢ ( 𝜑 → ( { 0 } ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑁 ‘ { 𝑇 } ) )
20 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
21 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
22 3 21 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23 20 16 22 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
24 21 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑇 } ) ∈ ( SubGrp ‘ 𝑈 ) )
25 20 23 24 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ∈ ( SubGrp ‘ 𝑈 ) )
26 10 4 lsm02 ⊢ ( ( 𝑁 ‘ { 𝑇 } ) ∈ ( SubGrp ‘ 𝑈 ) → ( { 0 } ⊕ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑁 ‘ { 𝑇 } ) )
27 25 26 syl ⊢ ( 𝜑 → ( { 0 } ⊕ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑁 ‘ { 𝑇 } ) )
28 19 27 eqtr4d ⊢ ( 𝜑 → ( { 0 } ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( { 0 } ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = { 0 } ) → ( { 0 } ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( { 0 } ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
30 14 29 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = { 0 } ) → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) = ( { 0 } ∨ ( 𝑁 ‘ { 𝑇 } ) ) )
31 13 30 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = { 0 } ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
32 20 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) → 𝑈 ∈ LMod )
33 1 2 6 3 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ 𝑉 )
34 8 9 33 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
35 3 21 lssss ⊢ ( ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑇 } ) ⊆ 𝑉 )
36 23 35 syl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ⊆ 𝑉 )
37 1 6 2 3 7 djhcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ ( 𝑁 ‘ { 𝑇 } ) ⊆ 𝑉 ) ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 )
38 8 34 36 37 syl12anc ⊢ ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 )
39 1 2 6 3 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ 𝑉 )
40 8 38 39 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ 𝑉 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ 𝑉 )
42 1 2 6 21 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
43 8 9 42 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
44 21 4 lsmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
45 20 43 23 44 syl3anc ⊢ ( 𝜑 → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
47 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑋 ≠ { 0 } )
48 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
49 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑋 ∈ ran 𝐼 )
50 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
51 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑇 ∈ ( 𝑉 ∖ { 0 } ) )
52 1 2 3 10 5 6 7 48 49 50 51 djhcvat42 ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑋 ≠ { 0 } ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) → ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) )
53 47 52 mpand ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) → ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) )
54 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 )
55 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → 𝑈 ∈ LMod )
56 43 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
57 eldifi ⊢ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) → 𝑦 ∈ 𝑉 )
58 57 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → 𝑦 ∈ 𝑉 )
59 3 21 5 55 56 58 lspsnel5 ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → ( 𝑦 ∈ 𝑋 ↔ ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ) )
60 54 59 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → 𝑦 ∈ 𝑋 )
61 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → 𝑇 ∈ 𝑉 )
62 3 5 lspsnid ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ) → 𝑇 ∈ ( 𝑁 ‘ { 𝑇 } ) )
63 55 61 62 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → 𝑇 ∈ ( 𝑁 ‘ { 𝑇 } ) )
64 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) )
65 sneq ⊢ ( 𝑧 = 𝑇 → { 𝑧 } = { 𝑇 } )
66 65 fveq2d ⊢ ( 𝑧 = 𝑇 → ( 𝑁 ‘ { 𝑧 } ) = ( 𝑁 ‘ { 𝑇 } ) )
67 66 oveq2d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) = ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) )
68 67 sseq2d ⊢ ( 𝑧 = 𝑇 → ( ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ↔ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) )
69 68 rspcev ⊢ ( ( 𝑇 ∈ ( 𝑁 ‘ { 𝑇 } ) ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) → ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) )
70 63 64 69 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) )
71 60 70 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) ) → ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) )
72 71 ex ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) → ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
73 72 reximdv2 ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑋 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) )
74 53 73 syld ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) )
75 74 anim2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
76 1 2 6 21 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ran 𝐼 ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
77 8 38 76 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
78 3 21 5 20 77 lspsnel6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑥 ∈ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ) ) )
80 3 21 4 5 20 43 23 lsmelval2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
81 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
82 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
83 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 ∈ 𝑋 )
84 3 21 lssel ⊢ ( ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑉 )
85 82 83 84 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 ∈ 𝑉 )
86 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
87 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) )
88 3 21 lssel ⊢ ( ( ( 𝑁 ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑧 ∈ 𝑉 )
89 86 87 88 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑧 ∈ 𝑉 )
90 1 2 3 4 5 6 7 81 85 89 djhlsmat ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) = ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) )
91 90 sseq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ↔ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) )
92 91 rexbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ↔ ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) )
93 92 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ↔ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) )
94 93 anbi2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
95 80 94 bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
96 95 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑥 ∈ ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑇 } ) ( 𝑁 ‘ { 𝑥 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ∨ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
97 75 79 96 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑥 ∈ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑥 ∈ ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ) )
98 10 21 32 41 46 97 lssssr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
99 1 2 3 4 7 8 34 36 djhsumss ⊢ ( 𝜑 → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) )
101 98 100 eqssd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ { 0 } ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
102 31 101 pm2.61dane ⊢ ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )