Step |
Hyp |
Ref |
Expression |
1 |
|
lcvexch.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) |
2 |
|
lcvexch.p |
⊢ ⊕ = ( LSSum ‘ 𝑊 ) |
3 |
|
lcvexch.c |
⊢ 𝐶 = ( ⋖L ‘ 𝑊 ) |
4 |
|
lcvexch.w |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
5 |
|
lcvexch.t |
⊢ ( 𝜑 → 𝑇 ∈ 𝑆 ) |
6 |
|
lcvexch.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑆 ) |
7 |
1
|
lsssssubg |
⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) ) |
8 |
4 7
|
syl |
⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) ) |
9 |
8 5
|
sseldd |
⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) |
10 |
8 6
|
sseldd |
⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) |
11 |
2
|
lsmub1 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
12 |
9 10 11
|
syl2anc |
⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
13 |
|
inss2 |
⊢ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 |
14 |
13
|
a1i |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ) |
15 |
12 14
|
2thd |
⊢ ( 𝜑 → ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ) ) |
16 |
2
|
lsmss2b |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑈 ⊆ 𝑇 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑇 ) ) |
17 |
9 10 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝑈 ⊆ 𝑇 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑇 ) ) |
18 |
|
eqcom |
⊢ ( ( 𝑇 ⊕ 𝑈 ) = 𝑇 ↔ 𝑇 = ( 𝑇 ⊕ 𝑈 ) ) |
19 |
17 18
|
syl6bb |
⊢ ( 𝜑 → ( 𝑈 ⊆ 𝑇 ↔ 𝑇 = ( 𝑇 ⊕ 𝑈 ) ) ) |
20 |
|
sseqin2 |
⊢ ( 𝑈 ⊆ 𝑇 ↔ ( 𝑇 ∩ 𝑈 ) = 𝑈 ) |
21 |
19 20
|
bitr3di |
⊢ ( 𝜑 → ( 𝑇 = ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) = 𝑈 ) ) |
22 |
21
|
necon3bid |
⊢ ( 𝜑 → ( 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) ≠ 𝑈 ) ) |
23 |
15 22
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ) ↔ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ∧ ( 𝑇 ∩ 𝑈 ) ≠ 𝑈 ) ) ) |
24 |
|
df-pss |
⊢ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ) ) |
25 |
|
df-pss |
⊢ ( ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ↔ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑈 ∧ ( 𝑇 ∩ 𝑈 ) ≠ 𝑈 ) ) |
26 |
23 24 25
|
3bitr4g |
⊢ ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ) ) |