Metamath Proof Explorer


Theorem lcvexchlem1

Description: Lemma for lcvexch . (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvexch.s S = LSubSp W
lcvexch.p ˙ = LSSum W
lcvexch.c C = L W
lcvexch.w φ W LMod
lcvexch.t φ T S
lcvexch.u φ U S
Assertion lcvexchlem1 φ T T ˙ U T U U

Proof

Step Hyp Ref Expression
1 lcvexch.s S = LSubSp W
2 lcvexch.p ˙ = LSSum W
3 lcvexch.c C = L W
4 lcvexch.w φ W LMod
5 lcvexch.t φ T S
6 lcvexch.u φ U S
7 1 lsssssubg W LMod S SubGrp W
8 4 7 syl φ S SubGrp W
9 8 5 sseldd φ T SubGrp W
10 8 6 sseldd φ U SubGrp W
11 2 lsmub1 T SubGrp W U SubGrp W T T ˙ U
12 9 10 11 syl2anc φ T T ˙ U
13 inss2 T U U
14 13 a1i φ T U U
15 12 14 2thd φ T T ˙ U T U U
16 sseqin2 U T T U = U
17 2 lsmss2b T SubGrp W U SubGrp W U T T ˙ U = T
18 9 10 17 syl2anc φ U T T ˙ U = T
19 eqcom T ˙ U = T T = T ˙ U
20 18 19 syl6bb φ U T T = T ˙ U
21 16 20 syl5rbbr φ T = T ˙ U T U = U
22 21 necon3bid φ T T ˙ U T U U
23 15 22 anbi12d φ T T ˙ U T T ˙ U T U U T U U
24 df-pss T T ˙ U T T ˙ U T T ˙ U
25 df-pss T U U T U U T U U
26 23 24 25 3bitr4g φ T T ˙ U T U U