Proof of Theorem lsppratlem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lspprat.w | . . . . 5
⊢ (𝜑 → 𝑊 ∈ LVec) | 
| 2 |  | lveclmod 21106 | . . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 4 |  | lspprat.v | . . . . 5
⊢ 𝑉 = (Base‘𝑊) | 
| 5 |  | lspprat.s | . . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) | 
| 6 |  | lspprat.n | . . . . 5
⊢ 𝑁 = (LSpan‘𝑊) | 
| 7 |  | lspprat.u | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑆) | 
| 8 | 4, 5 | lssss 20935 | . . . . . . . 8
⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) | 
| 9 | 7, 8 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ 𝑉) | 
| 10 | 9 | ssdifssd 4146 | . . . . . 6
⊢ (𝜑 → (𝑈 ∖ { 0 }) ⊆ 𝑉) | 
| 11 |  | lsppratlem1.x2 | . . . . . 6
⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) | 
| 12 | 10, 11 | sseldd 3983 | . . . . 5
⊢ (𝜑 → 𝑥 ∈ 𝑉) | 
| 13 | 9 | ssdifssd 4146 | . . . . . 6
⊢ (𝜑 → (𝑈 ∖ (𝑁‘{𝑥})) ⊆ 𝑉) | 
| 14 |  | lsppratlem1.y2 | . . . . . 6
⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) | 
| 15 | 13, 14 | sseldd 3983 | . . . . 5
⊢ (𝜑 → 𝑦 ∈ 𝑉) | 
| 16 | 4, 5, 6, 3, 12, 15 | lspprcl 20977 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑥, 𝑦}) ∈ 𝑆) | 
| 17 |  | df-pr 4628 | . . . . 5
⊢ {𝑥, 𝑌} = ({𝑥} ∪ {𝑌}) | 
| 18 |  | snsspr1 4813 | . . . . . . 7
⊢ {𝑥} ⊆ {𝑥, 𝑦} | 
| 19 | 12, 15 | prssd 4821 | . . . . . . . 8
⊢ (𝜑 → {𝑥, 𝑦} ⊆ 𝑉) | 
| 20 | 4, 6 | lspssid 20984 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ {𝑥, 𝑦} ⊆ 𝑉) → {𝑥, 𝑦} ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 21 | 3, 19, 20 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → {𝑥, 𝑦} ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 22 | 18, 21 | sstrid 3994 | . . . . . 6
⊢ (𝜑 → {𝑥} ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 23 | 12 | snssd 4808 | . . . . . . . . 9
⊢ (𝜑 → {𝑥} ⊆ 𝑉) | 
| 24 |  | lspprat.y | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 25 |  | lspprat.p | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) | 
| 26 | 25 | pssssd 4099 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘{𝑋, 𝑌})) | 
| 27 | 4, 5, 6, 3, 12, 24 | lspprcl 20977 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁‘{𝑥, 𝑌}) ∈ 𝑆) | 
| 28 |  | df-pr 4628 | . . . . . . . . . . . . . . 15
⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌}) | 
| 29 |  | lsppratlem4.x3 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌})) | 
| 30 | 29 | snssd 4808 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑋} ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 31 |  | snsspr2 4814 | . . . . . . . . . . . . . . . . 17
⊢ {𝑌} ⊆ {𝑥, 𝑌} | 
| 32 | 12, 24 | prssd 4821 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {𝑥, 𝑌} ⊆ 𝑉) | 
| 33 | 4, 6 | lspssid 20984 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ LMod ∧ {𝑥, 𝑌} ⊆ 𝑉) → {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 34 | 3, 32, 33 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 35 | 31, 34 | sstrid 3994 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 36 | 30, 35 | unssd 4191 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ({𝑋} ∪ {𝑌}) ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 37 | 28, 36 | eqsstrid 4021 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑋, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 38 | 5, 6 | lspssp 20987 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑥, 𝑌}) ∈ 𝑆 ∧ {𝑋, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 39 | 3, 27, 37, 38 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 40 | 26, 39 | sstrd 3993 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘{𝑥, 𝑌})) | 
| 41 | 17 | fveq2i 6908 | . . . . . . . . . . . 12
⊢ (𝑁‘{𝑥, 𝑌}) = (𝑁‘({𝑥} ∪ {𝑌})) | 
| 42 | 40, 41 | sseqtrdi 4023 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘({𝑥} ∪ {𝑌}))) | 
| 43 | 42 | ssdifd 4144 | . . . . . . . . . 10
⊢ (𝜑 → (𝑈 ∖ (𝑁‘{𝑥})) ⊆ ((𝑁‘({𝑥} ∪ {𝑌})) ∖ (𝑁‘{𝑥}))) | 
| 44 | 43, 14 | sseldd 3983 | . . . . . . . . 9
⊢ (𝜑 → 𝑦 ∈ ((𝑁‘({𝑥} ∪ {𝑌})) ∖ (𝑁‘{𝑥}))) | 
| 45 | 4, 5, 6 | lspsolv 21146 | . . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ ({𝑥} ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑦 ∈ ((𝑁‘({𝑥} ∪ {𝑌})) ∖ (𝑁‘{𝑥})))) → 𝑌 ∈ (𝑁‘({𝑥} ∪ {𝑦}))) | 
| 46 | 1, 23, 24, 44, 45 | syl13anc 1373 | . . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑁‘({𝑥} ∪ {𝑦}))) | 
| 47 |  | df-pr 4628 | . . . . . . . . 9
⊢ {𝑥, 𝑦} = ({𝑥} ∪ {𝑦}) | 
| 48 | 47 | fveq2i 6908 | . . . . . . . 8
⊢ (𝑁‘{𝑥, 𝑦}) = (𝑁‘({𝑥} ∪ {𝑦})) | 
| 49 | 46, 48 | eleqtrrdi 2851 | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑥, 𝑦})) | 
| 50 | 49 | snssd 4808 | . . . . . 6
⊢ (𝜑 → {𝑌} ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 51 | 22, 50 | unssd 4191 | . . . . 5
⊢ (𝜑 → ({𝑥} ∪ {𝑌}) ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 52 | 17, 51 | eqsstrid 4021 | . . . 4
⊢ (𝜑 → {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 53 | 5, 6 | lspssp 20987 | . . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑥, 𝑦}) ∈ 𝑆 ∧ {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑦})) → (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 54 | 3, 16, 52, 53 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦})) | 
| 55 | 54, 29 | sseldd 3983 | . 2
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑦})) | 
| 56 | 55, 49 | jca 511 | 1
⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))) |