Metamath Proof Explorer

Theorem oppglsm

Description: The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses oppglsm.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
oppglsm.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion oppglsm ( 𝑇 ( LSSum ‘ 𝑂 ) 𝑈 ) = ( 𝑈 ⊕ 𝑇 )

Proof

Step Hyp Ref Expression
1 oppglsm.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 oppglsm.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 1 fvexi ⊢ 𝑂 ∈ V
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 1 4 oppgbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑂 )
6 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
7 eqid ⊢ ( LSSum ‘ 𝑂 ) = ( LSSum ‘ 𝑂 )
8 5 6 7 lsmfval ⊢ ( 𝑂 ∈ V → ( LSSum ‘ 𝑂 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) ) )
9 3 8 ax-mp ⊢ ( LSSum ‘ 𝑂 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 4 10 2 lsmfval ⊢ ( 𝐺 ∈ V → ⊕ = ( 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
12 11 tposeqd ⊢ ( 𝐺 ∈ V → tpos ⊕ = tpos ( 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
13 eqid ⊢ ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
14 13 reldmmpo ⊢ Rel dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
15 13 mpofun ⊢ Fun ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
16 funforn ⊢ ( Fun ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) : dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) –onto→ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
17 15 16 mpbi ⊢ ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) : dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) –onto→ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
18 tposfo2 ⊢ ( Rel dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) → ( ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) : dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) –onto→ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) → tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) : ◡ dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) –onto→ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
19 14 17 18 mp2 ⊢ tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) : ◡ dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) –onto→ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
20 forn ⊢ ( tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) : ◡ dom ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) –onto→ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) → ran tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
21 19 20 ax-mp ⊢ ran tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
22 10 1 6 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 )
23 22 eqcomi ⊢ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 )
24 23 a1i ⊢ ( ( 𝑦 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
25 24 mpoeq3ia ⊢ ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
26 25 tposmpo ⊢ tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
27 26 rneqi ⊢ ran tpos ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
28 21 27 eqtr3i ⊢ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
29 28 a1i ⊢ ( ( 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) )
30 29 mpoeq3ia ⊢ ( 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) = ( 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) )
31 30 tposmpo ⊢ tpos ( 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑦 ∈ 𝑢 , 𝑥 ∈ 𝑡 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) )
32 12 31 eqtrdi ⊢ ( 𝐺 ∈ V → tpos ⊕ = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) ) )
33 9 32 eqtr4id ⊢ ( 𝐺 ∈ V → ( LSSum ‘ 𝑂 ) = tpos ⊕ )
34 33 oveqd ⊢ ( 𝐺 ∈ V → ( 𝑇 ( LSSum ‘ 𝑂 ) 𝑈 ) = ( 𝑇 tpos ⊕ 𝑈 ) )
35 ovtpos ⊢ ( 𝑇 tpos ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 )
36 34 35 eqtrdi ⊢ ( 𝐺 ∈ V → ( 𝑇 ( LSSum ‘ 𝑂 ) 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
37 eqid ⊢ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ )
38 0ex ⊢ ∅ ∈ V
39 eqidd ⊢ ( ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) → ∅ = ∅ )
40 37 38 39 elovmpo ⊢ ( 𝑥 ∈ ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) ↔ ( 𝑇 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑈 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ∅ ) )
41 40 simp3bi ⊢ ( 𝑥 ∈ ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) → 𝑥 ∈ ∅ )
42 41 ssriv ⊢ ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) ⊆ ∅
43 ss0 ⊢ ( ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) ⊆ ∅ → ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) = ∅ )
44 42 43 ax-mp ⊢ ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) = ∅
45 elpwi ⊢ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) → 𝑡 ⊆ ( Base ‘ 𝐺 ) )
46 45 3ad2ant2 ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → 𝑡 ⊆ ( Base ‘ 𝐺 ) )
47 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
48 47 3ad2ant1 ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∅ )
49 46 48 sseqtrd ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → 𝑡 ⊆ ∅ )
50 ss0 ⊢ ( 𝑡 ⊆ ∅ → 𝑡 = ∅ )
51 49 50 syl ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → 𝑡 = ∅ )
52 51 orcd ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → ( 𝑡 = ∅ ∨ 𝑢 = ∅ ) )
53 0mpo0 ⊢ ( ( 𝑡 = ∅ ∨ 𝑢 = ∅ ) → ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) = ∅ )
54 52 53 syl ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) = ∅ )
55 54 rneqd ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) = ran ∅ )
56 rn0 ⊢ ran ∅ = ∅
57 55 56 eqtrdi ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) ∧ 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ) → ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) = ∅ )
58 57 mpoeq3dva ⊢ ( ¬ 𝐺 ∈ V → ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ 𝑡 , 𝑦 ∈ 𝑢 ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) )
59 9 58 syl5eq ⊢ ( ¬ 𝐺 ∈ V → ( LSSum ‘ 𝑂 ) = ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) )
60 59 oveqd ⊢ ( ¬ 𝐺 ∈ V → ( 𝑇 ( LSSum ‘ 𝑂 ) 𝑈 ) = ( 𝑇 ( 𝑡 ∈ 𝒫 ( Base ‘ 𝐺 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝐺 ) ↦ ∅ ) 𝑈 ) )
61 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( LSSum ‘ 𝐺 ) = ∅ )
62 2 61 syl5eq ⊢ ( ¬ 𝐺 ∈ V → ⊕ = ∅ )
63 62 oveqd ⊢ ( ¬ 𝐺 ∈ V → ( 𝑈 ⊕ 𝑇 ) = ( 𝑈 ∅ 𝑇 ) )
64 0ov ⊢ ( 𝑈 ∅ 𝑇 ) = ∅
65 63 64 eqtrdi ⊢ ( ¬ 𝐺 ∈ V → ( 𝑈 ⊕ 𝑇 ) = ∅ )
66 44 60 65 3eqtr4a ⊢ ( ¬ 𝐺 ∈ V → ( 𝑇 ( LSSum ‘ 𝑂 ) 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
67 36 66 pm2.61i ⊢ ( 𝑇 ( LSSum ‘ 𝑂 ) 𝑈 ) = ( 𝑈 ⊕ 𝑇 )