This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dsmmval

Description: Value of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015)

Ref Expression
Hypothesis dsmmval.b ⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
Assertion dsmmval ( 𝑅 ∈ 𝑉 → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dsmmval.b ⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
2 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
3 oveq12 ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑠 Xs 𝑟 ) = ( 𝑆 Xs 𝑅 ) )
4 eqid ⊢ ( 𝑠 Xs 𝑟 ) = ( 𝑠 Xs 𝑟 )
5 vex ⊢ 𝑠 ∈ V
6 5 a1i ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑠 ∈ V )
7 vex ⊢ 𝑟 ∈ V
8 7 a1i ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑟 ∈ V )
9 eqid ⊢ ( Base ‘ ( 𝑠 Xs 𝑟 ) ) = ( Base ‘ ( 𝑠 Xs 𝑟 ) )
10 eqidd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → dom 𝑟 = dom 𝑟 )
11 4 6 8 9 10 prdsbas ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑠 Xs 𝑟 ) ) = X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) )
12 3 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑠 Xs 𝑟 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
13 11 12 eqtr3d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
14 simpr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
15 14 dmeqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → dom 𝑟 = dom 𝑅 )
16 14 fveq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑟 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) )
17 16 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
18 17 neeq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) ↔ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
19 15 18 rabeqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
20 19 eleq1d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin ↔ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) )
21 13 20 rabeqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } )
22 21 1 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } = 𝐵 )
23 3 22 oveq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
24 df-dsmm ⊢ ⊕m = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) )
25 ovex ⊢ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) ∈ V
26 23 24 25 ovmpoa ⊢ ( ( 𝑆 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
27 reldmdsmm ⊢ Rel dom ⊕m
28 27 ovprc1 ⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ∅ )
29 ress0 ⊢ ( ∅ ↾s 𝐵 ) = ∅
30 28 29 eqtr4di ⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ∅ ↾s 𝐵 ) )
31 reldmprds ⊢ Rel dom Xs
32 31 ovprc1 ⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 Xs 𝑅 ) = ∅ )
33 32 oveq1d ⊢ ( ¬ 𝑆 ∈ V → ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) = ( ∅ ↾s 𝐵 ) )
34 30 33 eqtr4d ⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
35 34 adantr ⊢ ( ( ¬ 𝑆 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
36 26 35 pm2.61ian ⊢ ( 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
37 2 36 syl ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )